company-coq-diff-unification-error: Stack overflow in regexp matcher #222

vzaliva · 2019-07-23T22:11:50Z

Executing company-coq-diff-unification-error got the following error "Stack overflow in regexp matcher"

The text was updated successfully, but these errors were encountered:

cpitclaudel · 2019-07-24T00:17:06Z

Oh no :(
Do you have an example of the input that led to that?

vzaliva · 2019-07-24T02:04:00Z

I will try to get you one. Just a copy of *response* buffer is what you need?

cpitclaudel · 2019-07-24T03:01:13Z

Yup, that should do

vzaliva · 2019-07-26T17:55:59Z

I refactored my code and could not reproduce it at the moment. I will keep an eye on it and will add a copy of the buffer next time it occurs.

cpitclaudel · 2019-07-26T18:10:27Z

Thanks.

vzaliva · 2019-08-07T00:21:50Z

Here it is:

Error: In environment
a : t CarrierA (S (S (S O)))
Unable to unify
 "@SH_MSH_Operator_compat ?i ?o Monoid_RthetaFlags ?a_zero
    (@HTSUMUnion Monoid_RthetaFlags ?i ?o ?a_zero ?dot ?dot_mor
       (@Monoid_BFixpoint ?dot ?a_zero ?M8940) ?M8933 ?M8934)
    (@MSigmaHCOL.MHTSUMUnion ?i ?o ?dot ?M8935 ?M8936)" with
 "@SH_MSH_Operator_compat (Init.Nat.add (S O) (S (S (S (S O)))))
    (Init.Nat.add (S O) (S O)) Monoid_RthetaFlags (@zero CarrierA CarrierAz)
    (@HTSUMUnion Monoid_RthetaFlags (Init.Nat.add (S O) (S (S (S (S O))))) 
       (S (S O)) (@zero CarrierA CarrierAz) CarrierAplus CarrierAPlus_proper
       Zero_Plus_BFixpoint
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (S (S (S (S O))))) (S O) (S (S O))
          (@eUnion Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
             (S (S O)) O (@le_S (S O) (S O) (le_n (S O))))
          (@SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S (S (S (S O)))))
             (S O)
             (@IReduction (@zero CarrierA CarrierAz)
                (Init.Nat.add (S O) (S (S (S (S O))))) (S O) 
                (S (S (S O))) CarrierAplus CarrierAPlus_proper Zero_Plus_BFixpoint
                (@SHFamilyOperatorCompose Monoid_RthetaSafeFlags
                   (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S (S (S (S O)))))
                   (S O) (S O) (S (S (S O)))
                   (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))) =>
                    @SHCompose Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
                      (S O) (S O) (S O)
                      (@SHPointwise Monoid_RthetaSafeFlags 
                         (@zero CarrierA CarrierAz) (S O)
                         (@Fin1SwapIndex CarrierA (S (S (S O))) jf
                            (@mult_by_nth (S (S (S O))) a))
                         (@Reflexive_partial_app_morphism
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (_ : CarrierA), CarrierA)
                            (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                               (_ : CarrierA), CarrierA)
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (forall _ : CarrierA, CarrierA)
                               (@equiv
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S (S O))))))
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe)))
                            (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (forall _ : CarrierA, CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S O))))
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe)))
                            (@Fin1SwapIndex CarrierA (S (S (S O))) jf)
                            (@Reflexive_partial_app_morphism
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (forall
                                  (_ : forall
                                         (_ : @sig nat
                                                (fun x : nat =>
                                                 Peano.lt x (S (S (S O)))))
                                         (_ : CarrierA), CarrierA)
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                  (_ : CarrierA), CarrierA)
                               (@equiv
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S (S O))))))
                               (@respectful
                                  (forall
                                     (_ : @sig nat
                                            (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (_ : CarrierA), CarrierA)
                                  (forall
                                     (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                     (_ : CarrierA), CarrierA)
                                  (@respectful
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (forall _ : CarrierA, CarrierA)
                                     (@equiv
                                        (@sig nat
                                           (fun x : nat => Peano.lt x (S (S (S O)))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S (S O))))))
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe)))
                                  (@respectful
                                     (@sig nat (fun x : nat => Peano.lt x (S O)))
                                     (forall _ : CarrierA, CarrierA)
                                     (@equiv
                                        (@sig nat (fun x : nat => Peano.lt x (S O)))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S O))))
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@Fin1SwapIndex CarrierA (S (S (S O))))
                               (@Fin1SwapIndex_proper CarrierA CarrierAe (S (S (S O))))
                               jf
                               (@reflexive_proper_proxy
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@equiv
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S (S O))))))
                                  (@Equivalence_Reflexive
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@equiv
                                        (@sig nat
                                           (fun x : nat => Peano.lt x (S (S (S O)))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S (S O))))))
                                     (@abstract_algebra.setoid_eq
                                        (@sig nat
                                           (fun x : nat => Peano.lt x (S (S (S O)))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S (S O)))))
                                        (@setoids.sig_setoid nat
                                           peano_naturals.nat_equiv
                                           (@abstract_algebra.sg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.comsg_setoid nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.semilattice_sg nat
                                                    peano_naturals.nat_equiv
                                                    (@meet_is_sg_op nat
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec)))
                                                    (@abstract_algebra.meet_semilattice
                                                       nat peano_naturals.nat_equiv
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.lattice_meet
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                           (fun x : nat => Peano.lt x (S (S (S O)))))))
                                  jf)) (@mult_by_nth (S (S (S O))) a)
                            (@proper_proper_proxy
                               (forall
                                  (_ : @sig nat
                                         (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (_ : CarrierA), CarrierA)
                               (@mult_by_nth (S (S (S O))) a)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (forall _ : CarrierA, CarrierA)
                                  (@equiv
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S (S O))))))
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe)))
                               (@mult_by_nth_proper (S (S (S O))) a))))
                      (@SHInductor Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz)
                         (@proj1_sig nat (fun x : nat => Peano.lt x (S (S (S O)))) jf)
                         (@mult CarrierA CarrierAmult)
                         (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                            CarrierAmult
                            (@abstract_algebra.monoid_semigroup CarrierA CarrierAe
                               CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                               (@abstract_algebra.commonoid_mon CarrierA CarrierAe
                                  CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                                  (@abstract_algebra.semimult_monoid CarrierA CarrierAe
                                     CarrierAplus CarrierAmult CarrierAz CarrierA1
                                     (@rings.Ring_Semi CarrierA CarrierAe CarrierAplus
                                        CarrierAmult CarrierAz CarrierA1 CarrierAneg
                                        CarrierAr))))) (@one CarrierA CarrierA1)))
                   (@eT Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz)
                      (Init.Nat.add (S O) (S (S (S (S O))))) O
                      (@GathH1_domain_bound_to_base_bound
                         (Init.Nat.add (S O) (S (S (S (S O))))) O 
                         (S O) (h_bound_first_half (S O) (S (S (S (S O)))))))))))
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (S (S (S (S O))))) (S O) (S (S O))
          (@eUnion Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
             (S (S O)) (S O) (le_n (S (S O))))
          (@SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S (S (S (S O)))))
             (S O)
             (@IReduction (@zero CarrierA CarrierAz)
                (Init.Nat.add (S O) (S (S (S (S O))))) (S O) 
                (S (S O)) (@minmax.max CarrierA CarrierAle CarrierAledec)
                (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                   (fun x y : CarrierA =>
                    @snd CarrierA CarrierA
                      (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                   (@abstract_algebra.comsg_setoid CarrierA CarrierAe
                      (fun x y : CarrierA =>
                       @snd CarrierA CarrierA
                         (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                      (@abstract_algebra.semilattice_sg CarrierA CarrierAe
                         (fun x y : CarrierA =>
                          @snd CarrierA CarrierA
                            (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                         (@abstract_algebra.join_semilattice CarrierA CarrierAe
                            (fun x y : CarrierA =>
                             @snd CarrierA CarrierA
                               (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                            (@abstract_algebra.lattice_join CarrierA CarrierAe
                               (fun x y : CarrierA =>
                                @snd CarrierA CarrierA
                                  (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                               (@minmax.min CarrierA CarrierAle CarrierAledec)
                               (@abstract_algebra.distr_lattice_lattice CarrierA
                                  CarrierAe
                                  (fun x y : CarrierA =>
                                   @snd CarrierA CarrierA
                                     (@minmax.sort CarrierA CarrierAle CarrierAledec x
                                        y))
                                  (@minmax.min CarrierA CarrierAle CarrierAledec)
                                  (@minmax.DistributiveLattice_instance_0 CarrierA
                                     CarrierAe CarrierAle CarrierAto CarrierAledec)))))))
                Zero_Max_BFixpoint
                (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @SHCompose Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz)
                   (Init.Nat.add (S O) (S (S (S (S O))))) (Init.Nat.add (S O) (S O))
                   (S O)
                   (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
                      (S O)
                      (fun (i : @sig nat (fun n : nat => Peano.lt n (S O)))
                         (a0 b : CarrierA) =>
                       @IgnoreIndex CarrierA (S O)
                         (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                            CarrierAabs) i
                         (@Fin1SwapIndex2 CarrierA (S (S O)) jf
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S O)))) sub) i
                            a0 b))
                      (@FinNat_f1_over_g2_proper (S O)
                         (@IgnoreIndex CarrierA (S O)
                            (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                               CarrierAabs))
                         (@Fin1SwapIndex2 CarrierA (S (S O)) jf
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S O)))) sub))
                         (@Reflexive_partial_app_morphism
                            (forall _ : CarrierA, CarrierA)
                            (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                               (_ : CarrierA), CarrierA)
                            (@respectful CarrierA CarrierA 
                               (@equiv CarrierA CarrierAe) 
                               (@equiv CarrierA CarrierAe))
                            (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (forall _ : CarrierA, CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S O))))
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe)))
                            (@IgnoreIndex CarrierA (S O))
                            (@IgnoredIndex_proper CarrierA CarrierAe (S O))
                            (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                               CarrierAabs)
                            (@proper_proper_proxy (forall _ : CarrierA, CarrierA)
                               (@abs CarrierA CarrierAe CarrierAle CarrierAz
                                  CarrierAneg CarrierAabs)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))
                               (@abstract_algebra.sm_proper CarrierA CarrierA CarrierAe
                                  CarrierAe
                                  (@abs CarrierA CarrierAe CarrierAle CarrierAz
                                     CarrierAneg CarrierAabs)
                                  (@abs_Setoid_Morphism CarrierA CarrierAe CarrierAplus
                                     CarrierAmult CarrierAz CarrierA1 CarrierAneg
                                     CarrierAr CarrierAsetoid CarrierAle CarrierAto
                                     CarrierAabs))))
                         (@Reflexive_partial_app_morphism
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S O))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@Fin1SwapIndex2 CarrierA (S (S O)) jf)
                            (@Reflexive_partial_app_morphism
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (forall
                                  (_ : forall
                                         (_ : @sig nat
                                                (fun x : nat => Peano.lt x (S (S O))))
                                         (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@respectful
                                  (forall
                                     (_ : @sig nat
                                            (fun x : nat => Peano.lt x (S (S O))))
                                     (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (forall
                                     (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                     (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@respectful
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                     (@equiv
                                        (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S O)))))
                                     (@respectful CarrierA
                                        (forall _ : CarrierA, CarrierA)
                                        (@equiv CarrierA CarrierAe)
                                        (@respectful CarrierA CarrierA
                                           (@equiv CarrierA CarrierAe)
                                           (@equiv CarrierA CarrierAe))))
                                  (@respectful
                                     (@sig nat (fun x : nat => Peano.lt x (S O)))
                                     (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                     (@equiv
                                        (@sig nat (fun x : nat => Peano.lt x (S O)))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S O))))
                                     (@respectful CarrierA
                                        (forall _ : CarrierA, CarrierA)
                                        (@equiv CarrierA CarrierAe)
                                        (@respectful CarrierA CarrierA
                                           (@equiv CarrierA CarrierAe)
                                           (@equiv CarrierA CarrierAe)))))
                               (@Fin1SwapIndex2 CarrierA (S (S O)))
                               (@Fin1SwapIndex2_proper CarrierA CarrierAe (S (S O))) jf
                               (@reflexive_proper_proxy
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@Equivalence_Reflexive
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@equiv
                                        (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S O)))))
                                     (@abstract_algebra.setoid_eq
                                        (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S O))))
                                        (@setoids.sig_setoid nat
                                           peano_naturals.nat_equiv
                                           (@abstract_algebra.sg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.comsg_setoid nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.semilattice_sg nat
                                                    peano_naturals.nat_equiv
                                                    (@meet_is_sg_op nat
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec)))
                                                    (@abstract_algebra.meet_semilattice
                                                       nat peano_naturals.nat_equiv
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.lattice_meet
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                           (fun x : nat => Peano.lt x (S (S O)))))) jf))
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S O)))) sub)
                            (@proper_proper_proxy
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@IgnoreIndex2 CarrierA
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O)))) sub)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@Reflexive_partial_app_morphism
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (forall
                                     (_ : @sig nat
                                            (fun x : nat => Peano.lt x (S (S O))))
                                     (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv (forall _ : CarrierA, CarrierA)
                                        (@ext_equiv CarrierA CarrierAe CarrierA
                                           CarrierAe)))
                                  (@respectful
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                     (@equiv
                                        (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                        (@Sig_Equiv nat peano_naturals.nat_equiv
                                           (fun x : nat => Peano.lt x (S (S O)))))
                                     (@respectful CarrierA
                                        (forall _ : CarrierA, CarrierA)
                                        (@equiv CarrierA CarrierAe)
                                        (@respectful CarrierA CarrierA
                                           (@equiv CarrierA CarrierAe)
                                           (@equiv CarrierA CarrierAe))))
                                  (@IgnoreIndex2 CarrierA
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O)))))
                                  (@IgnoreIndex2_proper CarrierA CarrierAe
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O))))) sub
                                  (@proper_proper_proxy
                                     (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                     sub
                                     (@respectful CarrierA
                                        (forall _ : CarrierA, CarrierA)
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv (forall _ : CarrierA, CarrierA)
                                           (@ext_equiv CarrierA CarrierAe CarrierA
                                              CarrierAe))) CarrierA_sub_proper))))))
                   (@UnSafeCast (@zero CarrierA CarrierAz)
                      (Init.Nat.add (S O) (S (S (S (S O))))) 
                      (S (S O))
                      (@ISumUnion (Init.Nat.add (S O) (S (S (S (S O))))) 
                         (S (S O)) (S (S O))
                         (fun jf0 : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                          @SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                            (Init.Nat.add (S O) (S (S (S (S O))))) 
                            (S O) (S (S O))
                            (@eUnion Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                               (S (S O))
                               (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                  jf0)
                               (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                  jf0))
                            (@eT Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                               (Init.Nat.add (S O) (S (S (S (S O)))))
                               (Init.Nat.add
                                  (Init.Nat.add (S O)
                                     (Init.Nat.mul
                                        (@proj1_sig nat
                                           (fun x : nat => Peano.lt x (S (S O))) jf)
                                        (S O)))
                                  (Init.Nat.mul
                                     (@proj1_sig nat
                                        (fun x : nat => Peano.lt x (S (S O))) jf0)
                                     (Init.Nat.mul (S (S O)) (S O))))
                               (@h_index_map_compose_range_bound
                                  (Init.Nat.add (S O) (S (S (S (S O))))) 
                                  (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                                  (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                     jf) (S O) (S (S O)) (S O)
                                  (GathH_jn_domain_bound
                                     (@proj1_sig nat
                                        (fun x : nat => Peano.lt x (S (S O))) jf)
                                     (S (S O))
                                     (@proj2_sig nat
                                        (fun x : nat => Peano.lt x (S (S O))) jf))
                                  (h_bound_second_half (S O) (S (S (S (S O)))))
                                  (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                     jf0)
                                  (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                     jf0)))))))))))
    (@MSigmaHCOL.MHTSUMUnion (Init.Nat.add (S O) (S (S (S (S O))))) 
       (S (S O)) CarrierAplus
       (@MSigmaHCOL.MSHCompose (Init.Nat.add (S O) (S (S (S (S O))))) 
          (S O) (S (S O))
          (@MSigmaHCOL.MSHeUnion (S (S O)) O (@le_S (S O) (S O) (le_n (S O))))
          (@MSigmaHCOL.MSHIReduction (Init.Nat.add (S O) (S (S (S (S O))))) 
             (S O) (S (S (S O))) (@zero CarrierA CarrierAz) CarrierAplus
             CarrierAPlus_proper
             (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))) =>
              @MSigmaHCOL.MSHCompose (Init.Nat.add (S O) (S (S (S (S O))))) 
                (S O) (S O)
                (@MSigmaHCOL.MSHCompose (S O) (S O) (S O)
                   (@MSigmaHCOL.MSHPointwise (S O)
                      (fun (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                         (x : CarrierA) =>
                       CarrierAmult x
                         (@Vnth CarrierA (S (S (S O))) a
                            (@proj1_sig nat (fun x0 : nat => Peano.lt x0 (S (S (S O))))
                               jf)
                            (@proj2_sig nat (fun x0 : nat => Peano.lt x0 (S (S (S O))))
                               jf)))
                      (@Reflexive_partial_app_morphism
                         (forall
                            (_ : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                            (_ : CarrierA), CarrierA)
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                            (_ : CarrierA), CarrierA)
                         (@respectful
                            (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                            (forall _ : CarrierA, CarrierA)
                            (@equiv
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S (S O))))))
                            (@respectful CarrierA CarrierA 
                               (@equiv CarrierA CarrierAe) 
                               (@equiv CarrierA CarrierAe)))
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                            (forall _ : CarrierA, CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S O))))
                            (@respectful CarrierA CarrierA 
                               (@equiv CarrierA CarrierAe) 
                               (@equiv CarrierA CarrierAe)))
                         (fun
                            (f : forall
                                   (_ : @sig nat
                                          (fun x : nat => Peano.lt x (S (S (S O)))))
                                   (_ : CarrierA), CarrierA)
                            (_ : @sig nat (fun x : nat => Peano.lt x (S O))) => 
                          f jf)
                         (@Reflexive_partial_app_morphism
                            (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                            (forall
                               (_ : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S (S O)))))
                                      (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                               (_ : CarrierA), CarrierA)
                            (@equiv
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S (S O))))))
                            (@respectful
                               (forall
                                  (_ : @sig nat
                                         (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (_ : CarrierA), CarrierA)
                               (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                  (_ : CarrierA), CarrierA)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (forall _ : CarrierA, CarrierA)
                                  (@equiv
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S (S O))))))
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe)))
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S O)))
                                  (forall _ : CarrierA, CarrierA)
                                  (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S O))))
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (fun
                               (i : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (f : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S (S O)))))
                                      (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun x : nat => Peano.lt x (S O))) => 
                             f i)
                            (@Fin1SwapIndex_proper CarrierA CarrierAe (S (S (S O)))) jf
                            (@reflexive_proper_proxy
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (@equiv
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S (S O))))))
                               (@Equivalence_Reflexive
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@equiv
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S (S O))))))
                                  (@abstract_algebra.setoid_eq
                                     (@sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                                     (@setoids.sig_setoid nat peano_naturals.nat_equiv
                                        (@abstract_algebra.sg_setoid nat
                                           peano_naturals.nat_equiv
                                           (@meet_is_sg_op nat
                                              (@minmax.min nat
                                                 (@le nat peano_naturals.nat_le)
                                                 (@peano_naturals.nat_le_dec)))
                                           (@abstract_algebra.comsg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.semilattice_sg nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.meet_semilattice
                                                    nat peano_naturals.nat_equiv
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec))
                                                    (@abstract_algebra.lattice_meet nat
                                                       peano_naturals.nat_equiv
                                                       (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                        (fun x : nat => Peano.lt x (S (S (S O))))))) jf))
                         (fun
                            (jf0 : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                            (x : CarrierA) =>
                          CarrierAmult x
                            (@Vnth CarrierA (S (S (S O))) a
                               (@proj1_sig nat
                                  (fun x0 : nat => Peano.lt x0 (S (S (S O)))) jf0)
                               (@proj2_sig nat
                                  (fun x0 : nat => Peano.lt x0 (S (S (S O)))) jf0)))
                         (@proper_proper_proxy
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (_ : CarrierA), CarrierA)
                            (fun
                               (jf0 : @sig nat
                                        (fun x : nat => Peano.lt x (S (S (S O)))))
                               (x : CarrierA) =>
                             CarrierAmult x
                               (@Vnth CarrierA (S (S (S O))) a
                                  (@proj1_sig nat
                                     (fun x0 : nat => Peano.lt x0 (S (S (S O)))) jf0)
                                  (@proj2_sig nat
                                     (fun x0 : nat => Peano.lt x0 (S (S (S O)))) jf0)))
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (forall _ : CarrierA, CarrierA)
                               (@equiv
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S (S O))))))
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe)))
                            (@mult_by_nth_proper (S (S (S O))) a))))
                   (@MSigmaHCOL.MSHInductor
                      (@proj1_sig nat (fun x : nat => Peano.lt x (S (S (S O)))) jf)
                      CarrierAmult
                      (@abstract_algebra.sg_op_proper CarrierA CarrierAe CarrierAmult
                         (@abstract_algebra.monoid_semigroup CarrierA CarrierAe
                            CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                            (@abstract_algebra.commonoid_mon CarrierA CarrierAe
                               CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                               (@abstract_algebra.semimult_monoid CarrierA CarrierAe
                                  CarrierAplus CarrierAmult CarrierAz CarrierA1
                                  (@rings.Ring_Semi CarrierA CarrierAe CarrierAplus
                                     CarrierAmult CarrierAz CarrierA1 CarrierAneg
                                     CarrierAr))))) (@one CarrierA CarrierA1)))
                (@MSigmaHCOL.MSHeT (Init.Nat.add (S O) (S (S (S (S O))))) O
                   (@GathH1_domain_bound_to_base_bound
                      (Init.Nat.add (S O) (S (S (S (S O))))) O 
                      (S O) (h_bound_first_half (S O) (S (S (S (S O))))))))))
       (@MSigmaHCOL.MSHCompose (Init.Nat.add (S O) (S (S (S (S O))))) 
          (S O) (S (S O)) (@MSigmaHCOL.MSHeUnion (S (S O)) (S O) (le_n (S (S O))))
          (@MSigmaHCOL.MSHIReduction (Init.Nat.add (S O) (S (S (S (S O))))) 
             (S O) (S (S O)) (@zero CarrierA CarrierAz)
             (@minmax.max CarrierA CarrierAle CarrierAledec)
             (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                (fun x y : CarrierA =>
                 @snd CarrierA CarrierA
                   (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                (@abstract_algebra.comsg_setoid CarrierA CarrierAe
                   (fun x y : CarrierA =>
                    @snd CarrierA CarrierA
                      (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                   (@abstract_algebra.semilattice_sg CarrierA CarrierAe
                      (fun x y : CarrierA =>
                       @snd CarrierA CarrierA
                         (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                      (@abstract_algebra.join_semilattice CarrierA CarrierAe
                         (fun x y : CarrierA =>
                          @snd CarrierA CarrierA
                            (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                         (@abstract_algebra.lattice_join CarrierA CarrierAe
                            (fun x y : CarrierA =>
                             @snd CarrierA CarrierA
                               (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                            (@minmax.min CarrierA CarrierAle CarrierAledec)
                            (@abstract_algebra.distr_lattice_lattice CarrierA CarrierAe
                               (fun x y : CarrierA =>
                                @snd CarrierA CarrierA
                                  (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                               (@minmax.min CarrierA CarrierAle CarrierAledec)
                               (@minmax.DistributiveLattice_instance_0 CarrierA
                                  CarrierAe CarrierAle CarrierAto CarrierAledec)))))))
             (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
              @MSigmaHCOL.MSHCompose (Init.Nat.add (S O) (S (S (S (S O)))))
                (Init.Nat.add (S O) (S O)) (S O)
                (@MSigmaHCOL.MSHBinOp (S O)
                   (fun (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                      (a0 b : CarrierA) =>
                    @abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                      CarrierAabs (sub a0 b))
                   (@FinNat_f1_over_g2_proper (S O)
                      (fun
                         _ : @sig nat
                               (fun i : nat => @lt nat peano_naturals.nat_lt i (S O))
                       =>
                       @abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                         CarrierAabs)
                      (fun _ : @sig nat (fun x : nat => Peano.lt x (S O)) => sub)
                      (@Reflexive_partial_app_morphism (forall _ : CarrierA, CarrierA)
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                            (_ : CarrierA), CarrierA)
                         (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                            (@equiv CarrierA CarrierAe))
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                            (forall _ : CarrierA, CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S O))))
                            (@respectful CarrierA CarrierA 
                               (@equiv CarrierA CarrierAe) 
                               (@equiv CarrierA CarrierAe)))
                         (fun (f : forall _ : CarrierA, CarrierA)
                            (_ : @sig nat
                                   (fun i : nat =>
                                    @lt nat peano_naturals.nat_lt i (S O))) => f)
                         (@IgnoredIndex_proper CarrierA CarrierAe (S O))
                         (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                            CarrierAabs)
                         (@proper_proper_proxy (forall _ : CarrierA, CarrierA)
                            (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                               CarrierAabs)
                            (@respectful CarrierA CarrierA 
                               (@equiv CarrierA CarrierAe) 
                               (@equiv CarrierA CarrierAe))
                            (@abstract_algebra.sm_proper CarrierA CarrierA CarrierAe
                               CarrierAe
                               (@abs CarrierA CarrierAe CarrierAle CarrierAz
                                  CarrierAneg CarrierAabs)
                               (@abs_Setoid_Morphism CarrierA CarrierAe CarrierAplus
                                  CarrierAmult CarrierAz CarrierA1 CarrierAneg
                                  CarrierAr CarrierAsetoid CarrierAle CarrierAto
                                  CarrierAabs))))
                      (@Reflexive_partial_app_morphism
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S O))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (fun
                            (f : forall
                                   (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                   (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (_ : @sig nat (fun x : nat => Peano.lt x (S O))) => 
                          f jf)
                         (@Reflexive_partial_app_morphism
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall
                               (_ : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S O))))
                                      (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O)))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S O)))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S O))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe)))))
                            (fun (i : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (f : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S O))))
                                      (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun x : nat => Peano.lt x (S O))) => 
                             f i) (@Fin1SwapIndex2_proper CarrierA CarrierAe (S (S O)))
                            jf
                            (@reflexive_proper_proxy
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@Equivalence_Reflexive
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@abstract_algebra.setoid_eq
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O))))
                                     (@setoids.sig_setoid nat peano_naturals.nat_equiv
                                        (@abstract_algebra.sg_setoid nat
                                           peano_naturals.nat_equiv
                                           (@meet_is_sg_op nat
                                              (@minmax.min nat
                                                 (@le nat peano_naturals.nat_le)
                                                 (@peano_naturals.nat_le_dec)))
                                           (@abstract_algebra.comsg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.semilattice_sg nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.meet_semilattice
                                                    nat peano_naturals.nat_equiv
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec))
                                                    (@abstract_algebra.lattice_meet nat
                                                       peano_naturals.nat_equiv
                                                       (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                        (fun x : nat => Peano.lt x (S (S O)))))) jf))
                         (fun _ : @sig nat (fun x : nat => Peano.lt x (S (S O))) => sub)
                         (@proper_proper_proxy
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (fun _ : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                             sub)
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@Reflexive_partial_app_morphism
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv (forall _ : CarrierA, CarrierA)
                                     (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (fun
                                  (f : forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                => f)
                               (@IgnoreIndex2_proper CarrierA CarrierAe
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O))))) sub
                               (@proper_proper_proxy
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA) sub
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv (forall _ : CarrierA, CarrierA)
                                        (@ext_equiv CarrierA CarrierAe CarrierA
                                           CarrierAe))) CarrierA_sub_proper))))))
                (@MSigmaHCOL.MSHIUnion (Init.Nat.add (S O) (S (S (S (S O))))) 
                   (S (S O)) (S (S O))
                   (fun jf0 : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                    @MSigmaHCOL.MSHCompose (Init.Nat.add (S O) (S (S (S (S O))))) 
                      (S O) (S (S O))
                      (@MSigmaHCOL.MSHeUnion (S (S O))
                         (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) jf0)
                         (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) jf0))
                      (@MSigmaHCOL.MSHeT (Init.Nat.add (S O) (S (S (S (S O)))))
                         (Init.Nat.add
                            (Init.Nat.add (S O)
                               (Init.Nat.mul
                                  (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                     jf) (S O)))
                            (Init.Nat.mul
                               (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O)))
                                  jf0) (Init.Nat.mul (S (S O)) (S O))))
                         (@h_index_map_compose_range_bound
                            (Init.Nat.add (S O) (S (S (S (S O))))) 
                            (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                            (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) jf)
                            (S O) (S (S O)) (S O)
                            (GathH_jn_domain_bound
                               (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) jf)
                               (S (S O))
                               (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) jf))
                            (h_bound_second_half (S O) (S (S (S (S O)))))
                            (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) jf0)
                            (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) jf0)))))))))".

vzaliva · 2019-11-27T02:34:43Z

Another example:

Error: In environment
a : t CarrierA (S (S (S O)))
Unable to unify
 "@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
    (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
    (Init.Nat.add (S O) (S O)) (S O)
    (@SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S O)) 
       (S O)
       (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
          (S O)
          (@IgnoreIndex2 CarrierA (@sig nat (fun n : nat => Peano.lt n (S O))) Zless)
          (@Reflexive_partial_app_morphism
             (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
             (forall (_ : @sig nat (fun n : nat => Peano.lt n (S O))) 
                (_ : CarrierA) (_ : CarrierA), CarrierA)
             (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                (@equiv CarrierA CarrierAe)
                (@equiv (forall _ : CarrierA, CarrierA)
                   (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
             (@respectful (@sig nat (fun n : nat => Peano.lt n (S O)))
                (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                (@equiv (@sig nat (fun n : nat => Peano.lt n (S O)))
                   (@Sig_Equiv nat peano_naturals.nat_equiv
                      (fun n : nat => Peano.lt n (S O))))
                (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                   (@equiv CarrierA CarrierAe)
                   (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                      (@equiv CarrierA CarrierAe))))
             (@IgnoreIndex2 CarrierA (@sig nat (fun n : nat => Peano.lt n (S O))))
             (@IgnoreIndex2_proper CarrierA CarrierAe
                (@sig nat (fun n : nat => Peano.lt n (S O)))
                (@Sig_Equiv nat peano_naturals.nat_equiv
                   (fun n : nat => Peano.lt n (S O)))) Zless
             (@proper_proper_proxy (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                Zless
                (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                   (@equiv CarrierA CarrierAe)
                   (@equiv (forall _ : CarrierA, CarrierA)
                      (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe))) Zless_proper))))
    (@HTSUMUnion Monoid_RthetaFlags
       (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
       (Init.Nat.add (S O) (S O)) (@zero CarrierA CarrierAz)
       (@plus CarrierA CarrierAplus) CarrierAPlus_proper Zero_Plus_BFixpoint
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
          (S O) (Init.Nat.add (S O) (S O))
          (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
             (S O) (S (S (S O))) (Init.Nat.add (S O) (S O))
             (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                (S (S (S O))) (Init.Nat.add (S (S (S O))) (S (S (S O))))
                (Init.Nat.add (S O) (S O))
                (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                   (Init.Nat.add (S (S (S O))) (S (S (S O)))) 
                   (S (S (S O))) (Init.Nat.add (S O) (S O))
                   (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                      (S (S (S O))) (S O) (Init.Nat.add (S O) (S O))
                      (@ScatH Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                         (S O) (Init.Nat.add (S O) (S O)) O 
                         (S O) (h_bound_first_half (S O) (S O))
                         (@ScatH_stride1_constr (S O) (S (S O))))
                      (@liftM_HOperator Monoid_RthetaFlags 
                         (S (S (S O))) (S O) (@zero CarrierA CarrierAz)
                         (@HReduction (S (S (S O))) (@plus CarrierA CarrierAplus)
                            (@zero CarrierA CarrierAz))
                         (@HReduction_HOperator (S (S (S O)))
                            (@plus CarrierA CarrierAplus) CarrierAPlus_proper
                            (@zero CarrierA CarrierAz))))
                   (@SafeCast (@zero CarrierA CarrierAz)
                      (Init.Nat.add (S (S (S O))) (S (S (S O)))) 
                      (S (S (S O)))
                      (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz)
                         (S (S (S O)))
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun n : nat => Peano.lt n (S (S (S O)))))
                            (@mult CarrierA CarrierAmult))
                         (@Reflexive_partial_app_morphism
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (forall
                               (_ : @sig nat (fun n : nat => Peano.lt n (S (S (S O)))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@equiv (forall _ : CarrierA, CarrierA)
                                  (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                            (@respectful
                               (@sig nat (fun n : nat => Peano.lt n (S (S (S O)))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv
                                  (@sig nat (fun n : nat => Peano.lt n (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun n : nat => Peano.lt n (S (S (S O))))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun n : nat => Peano.lt n (S (S (S O))))))
                            (@IgnoreIndex2_proper CarrierA CarrierAe
                               (@sig nat (fun n : nat => Peano.lt n (S (S (S O)))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun n : nat => Peano.lt n (S (S (S O))))))
                            (@mult CarrierA CarrierAmult)
                            (@proper_proper_proxy
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@mult CarrierA CarrierAmult)
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv (forall _ : CarrierA, CarrierA)
                                     (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                               (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                                  CarrierAmult
                                  (@abstract_algebra.monoid_semigroup CarrierA
                                     CarrierAe CarrierAmult
                                     (@one_is_mon_unit CarrierA CarrierA1)
                                     (@abstract_algebra.commonoid_mon CarrierA
                                        CarrierAe CarrierAmult
                                        (@one_is_mon_unit CarrierA CarrierA1)
                                        (@abstract_algebra.semimult_monoid CarrierA
                                           CarrierAe CarrierAplus CarrierAmult
                                           CarrierAz CarrierA1
                                           (@rings.Ring_Semi CarrierA CarrierAe
                                              CarrierAplus CarrierAmult CarrierAz
                                              CarrierA1 CarrierAneg CarrierAr))))))))))
                (@liftM_HOperator Monoid_RthetaFlags (S (S (S O)))
                   (Init.Nat.add (S (S (S O))) (S (S (S O))))
                   (@zero CarrierA CarrierAz) (@HPrepend (S (S (S O))) (S (S (S O))) a)
                   (@HPrepend_HOperator (S (S (S O))) (S (S (S O))) a)))
             (@liftM_HOperator Monoid_RthetaFlags (S O) (S (S (S O)))
                (@zero CarrierA CarrierAz)
                (HInduction (S (S (S O))) (@mult CarrierA CarrierAmult)
                   (@one CarrierA CarrierA1))
                (@HInduction_HOperator (S (S (S O))) (@mult CarrierA CarrierAmult)
                   (@abstract_algebra.sg_op_proper CarrierA CarrierAe CarrierAmult
                      (@abstract_algebra.monoid_semigroup CarrierA CarrierAe
                         CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                         (@abstract_algebra.commonoid_mon CarrierA CarrierAe
                            CarrierAmult (@one_is_mon_unit CarrierA CarrierA1)
                            (@abstract_algebra.semimult_monoid CarrierA CarrierAe
                               CarrierAplus CarrierAmult CarrierAz CarrierA1
                               (@rings.Ring_Semi CarrierA CarrierAe CarrierAplus
                                  CarrierAmult CarrierAz CarrierA1 CarrierAneg
                                  CarrierAr))))) (@one CarrierA CarrierA1))))
          (@GathH Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
             (S O) O (S O)
             (h_bound_first_half (S O) (Init.Nat.add (S (S O)) (S (S O))))))
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
          (Init.Nat.add (S (S O)) (S (S O))) (Init.Nat.add (S O) (S O))
          (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S (S O)) (S (S O))) (S (S O)) (Init.Nat.add (S O) (S O))
             (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                (S (S O)) (S (S O)) (Init.Nat.add (S O) (S O))
                (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                   (S (S O)) (S O) (Init.Nat.add (S O) (S O))
                   (@ScatH Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                      (S O) (Init.Nat.add (S O) (S O)) (S O) 
                      (S O) (h_bound_second_half (S O) (S O))
                      (@ScatH_stride1_constr (S O) (S (S O))))
                   (@liftM_HOperator Monoid_RthetaFlags (S (S O)) 
                      (S O) (@zero CarrierA CarrierAz)
                      (@HReduction (S (S O))
                         (@minmax.max CarrierA CarrierAle CarrierAledec)
                         (@zero CarrierA CarrierAz))
                      (@HReduction_HOperator (S (S O))
                         (@minmax.max CarrierA CarrierAle CarrierAledec)
                         (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                            (fun x y : CarrierA =>
                             @snd CarrierA CarrierA
                               (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                            (@abstract_algebra.comsg_setoid CarrierA CarrierAe
                               (fun x y : CarrierA =>
                                @snd CarrierA CarrierA
                                  (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                               (@abstract_algebra.semilattice_sg CarrierA CarrierAe
                                  (fun x y : CarrierA =>
                                   @snd CarrierA CarrierA
                                     (@minmax.sort CarrierA CarrierAle CarrierAledec x
                                        y))
                                  (@abstract_algebra.join_semilattice CarrierA
                                     CarrierAe
                                     (fun x y : CarrierA =>
                                      @snd CarrierA CarrierA
                                        (@minmax.sort CarrierA CarrierAle CarrierAledec
                                           x y))
                                     (@abstract_algebra.lattice_join CarrierA CarrierAe
                                        (fun x y : CarrierA =>
                                         @snd CarrierA CarrierA
                                           (@minmax.sort CarrierA CarrierAle
                                              CarrierAledec x y))
                                        (@minmax.min CarrierA CarrierAle CarrierAledec)
                                        (@abstract_algebra.distr_lattice_lattice
                                           CarrierA CarrierAe
                                           (fun x y : CarrierA =>
                                            @snd CarrierA CarrierA
                                              (@minmax.sort CarrierA CarrierAle
                                                 CarrierAledec x y))
                                           (@minmax.min CarrierA CarrierAle
                                              CarrierAledec)
                                           (@minmax.DistributiveLattice_instance_0
                                              CarrierA CarrierAe CarrierAle CarrierAto
                                              CarrierAledec)))))))
                         (@zero CarrierA CarrierAz))))
                (@SHPointwise Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                   (S (S O))
                   (@IgnoreIndex CarrierA (S (S O))
                      (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                         CarrierAabs))
                   (@Reflexive_partial_app_morphism (forall _ : CarrierA, CarrierA)
                      (forall (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                         (_ : CarrierA), CarrierA)
                      (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                         (@equiv CarrierA CarrierAe))
                      (@respectful (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                         (forall _ : CarrierA, CarrierA)
                         (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@Sig_Equiv nat peano_naturals.nat_equiv
                               (fun x : nat => Peano.lt x (S (S O)))))
                         (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                            (@equiv CarrierA CarrierAe)))
                      (@IgnoreIndex CarrierA (S (S O)))
                      (@IgnoredIndex_proper CarrierA CarrierAe (S (S O)))
                      (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                         CarrierAabs)
                      (@proper_proper_proxy (forall _ : CarrierA, CarrierA)
                         (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                            CarrierAabs)
                         (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                            (@equiv CarrierA CarrierAe))
                         (@abstract_algebra.sm_proper CarrierA CarrierA CarrierAe
                            CarrierAe
                            (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                               CarrierAabs)
                            (@abs_Setoid_Morphism CarrierA CarrierAe CarrierAplus
                               CarrierAmult CarrierAz CarrierA1 CarrierAneg CarrierAr
                               CarrierAsetoid CarrierAle CarrierAto CarrierAabs))))))
             (@SumSparseEmbedding (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                (S (S O)) (Init.Nat.add (S O) (S O)) (S O)
                (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S O)) 
                   (S O)
                   (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
                      (S O)
                      (@Fin1SwapIndex2 CarrierA (S (S O)) jf
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@sub CarrierA CarrierAplus CarrierAneg)))
                      (@Reflexive_partial_app_morphism
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (forall (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (@respectful (@sig nat (fun n : nat => Peano.lt n (S O)))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun n : nat => Peano.lt n (S O)))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun n : nat => Peano.lt n (S O))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (@Fin1SwapIndex2 CarrierA (S (S O)) jf)
                         (@Reflexive_partial_app_morphism
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall
                               (_ : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S O))))
                                      (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@respectful
                                  (@sig nat (fun n : nat => Peano.lt n (S O)))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv (@sig nat (fun n : nat => Peano.lt n (S O)))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun n : nat => Peano.lt n (S O))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe)))))
                            (@Fin1SwapIndex2 CarrierA (S (S O)))
                            (@Fin1SwapIndex2_proper CarrierA CarrierAe (S (S O))) jf
                            (@reflexive_proper_proxy
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@Equivalence_Reflexive
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@abstract_algebra.setoid_eq
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O))))
                                     (@setoids.sig_setoid nat peano_naturals.nat_equiv
                                        (@abstract_algebra.sg_setoid nat
                                           peano_naturals.nat_equiv
                                           (@meet_is_sg_op nat
                                              (@minmax.min nat
                                                 (@le nat peano_naturals.nat_le)
                                                 (@peano_naturals.nat_le_dec)))
                                           (@abstract_algebra.comsg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.semilattice_sg nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.meet_semilattice
                                                    nat peano_naturals.nat_equiv
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec))
                                                    (@abstract_algebra.lattice_meet nat
                                                       peano_naturals.nat_equiv
                                                       (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                        (fun x : nat => Peano.lt x (S (S O)))))) jf))
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@sub CarrierA CarrierAplus CarrierAneg))
                         (@proper_proper_proxy
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@sub CarrierA CarrierAplus CarrierAneg))
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@Reflexive_partial_app_morphism
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv (forall _ : CarrierA, CarrierA)
                                     (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@IgnoreIndex2 CarrierA
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O)))))
                               (@IgnoreIndex2_proper CarrierA CarrierAe
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@sub CarrierA CarrierAplus CarrierAneg)
                               (@proper_proper_proxy
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@sub CarrierA CarrierAplus CarrierAneg)
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv (forall _ : CarrierA, CarrierA)
                                        (@ext_equiv CarrierA CarrierAe CarrierA
                                           CarrierAe))) CarrierA_sub_proper))))))
                (fun j : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @h_index_map (S O) (S (S O))
                   (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j) 
                   (S O)
                   (ScatH_1_to_n_range_bound
                      (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j)
                      (S (S O)) (S O)
                      (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) j)))
                (@h_j_1_family_injective (S (S O)))
                (fun j : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @h_index_map (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                   (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j) 
                   (S (S O))
                   (GathH_jn_domain_bound
                      (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j)
                      (S (S O))
                      (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) j)))))
          (@GathH Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
             (Init.Nat.add (S (S O)) (S (S O))) (S O) (S O)
             (h_bound_second_half (S O) (Init.Nat.add (S (S O)) (S (S O)))))))" with
 "@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
    (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
    (Init.Nat.add (S O) (S O)) (S O)
    (@SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S O)) 
       (S O)
       (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
          (S O)
          (@IgnoreIndex2 CarrierA (@sig nat (fun x : nat => Peano.lt x (S O))) Zless)
          (@Reflexive_partial_app_morphism
             (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
             (forall (_ : @sig nat (fun x : nat => Peano.lt x (S O))) 
                (_ : CarrierA) (_ : CarrierA), CarrierA)
             (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                (@equiv CarrierA CarrierAe)
                (@equiv (forall _ : CarrierA, CarrierA)
                   (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
             (@respectful (@sig nat (fun x : nat => Peano.lt x (S O)))
                (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                (@equiv (@sig nat (fun x : nat => Peano.lt x (S O)))
                   (@Sig_Equiv nat peano_naturals.nat_equiv
                      (fun x : nat => Peano.lt x (S O))))
                (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                   (@equiv CarrierA CarrierAe)
                   (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                      (@equiv CarrierA CarrierAe))))
             (@IgnoreIndex2 CarrierA (@sig nat (fun x : nat => Peano.lt x (S O))))
             (@IgnoreIndex2_proper CarrierA CarrierAe
                (@sig nat (fun x : nat => Peano.lt x (S O)))
                (@Sig_Equiv nat peano_naturals.nat_equiv
                   (fun x : nat => Peano.lt x (S O)))) Zless
             (@proper_proper_proxy (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                Zless
                (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                   (@equiv CarrierA CarrierAe)
                   (@equiv (forall _ : CarrierA, CarrierA)
                      (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe))) Zless_proper))))
    (@HTSUMUnion Monoid_RthetaFlags
       (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
       (Init.Nat.add (S O) (S O)) (@zero CarrierA CarrierAz)
       (@plus CarrierA CarrierAplus) CarrierAPlus_proper Zero_Plus_BFixpoint
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
          (S O) (Init.Nat.add (S O) (S O))
          (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
             (S O) (S (S (S O))) (Init.Nat.add (S O) (S O))
             (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                (S (S (S O))) (Init.Nat.add (S (S (S O))) (S (S (S O))))
                (Init.Nat.add (S O) (S O))
                (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                   (Init.Nat.add (S (S (S O))) (S (S (S O)))) 
                   (S (S (S O))) (Init.Nat.add (S O) (S O))
                   (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
                      (S (S (S O))) (S O) (Init.Nat.add (S O) (S O))
                      (@ScatH Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                         (S O) (Init.Nat.add (S O) (S O)) O 
                         (S O) (h_bound_first_half (S O) (S O))
                         (@ScatH_stride1_constr (S O) (S (S O))))
                      (@liftM_HOperator Monoid_RthetaFlags 
                         (S (S (S O))) (S O) (@zero CarrierA CarrierAz)
                         (@HReduction (S (S (S O))) (@plus CarrierA CarrierAplus)
                            (@zero CarrierA CarrierAz))
                         (@HReduction_HOperator (S (S (S O)))
                            (@plus CarrierA CarrierAplus)
                            MDSigmaHCOLEvalSigCarrierA.plus_proper
                            (@zero CarrierA CarrierAz))))
                   (@SafeCast (@zero CarrierA CarrierAz)
                      (Init.Nat.add (S (S (S O))) (S (S (S O)))) 
                      (S (S (S O)))
                      (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz)
                         (S (S (S O)))
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                            (@mult CarrierA CarrierAmult))
                         (@Reflexive_partial_app_morphism
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@equiv (forall _ : CarrierA, CarrierA)
                                  (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv
                                  (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S (S O))))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O))))))
                            (@IgnoreIndex2_proper CarrierA CarrierAe
                               (@sig nat (fun x : nat => Peano.lt x (S (S (S O)))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S (S O))))))
                            (@mult CarrierA CarrierAmult)
                            (@proper_proper_proxy
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@mult CarrierA CarrierAmult)
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv (forall _ : CarrierA, CarrierA)
                                     (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                               MDSigmaHCOLEvalSigCarrierA.mult_proper)))))
                (@liftM_HOperator Monoid_RthetaFlags (S (S (S O)))
                   (Init.Nat.add (S (S (S O))) (S (S (S O))))
                   (@zero CarrierA CarrierAz) (@HPrepend (S (S (S O))) (S (S (S O))) a)
                   (@HPrepend_HOperator (S (S (S O))) (S (S (S O))) a)))
             (@liftM_HOperator Monoid_RthetaFlags (S O) (S (S (S O)))
                (@zero CarrierA CarrierAz)
                (HInduction (S (S (S O))) (@mult CarrierA CarrierAmult)
                   (@one CarrierA CarrierA1))
                (@HInduction_HOperator (S (S (S O))) (@mult CarrierA CarrierAmult)
                   MDSigmaHCOLEvalSigCarrierA.mult_proper (@one CarrierA CarrierA1))))
          (@GathH Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O)))) 
             (S O) O (S O)
             (h_bound_first_half (S O) (Init.Nat.add (S (S O)) (S (S O))))))
       (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
          (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
          (Init.Nat.add (S (S O)) (S (S O))) (Init.Nat.add (S O) (S O))
          (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S (S O)) (S (S O))) (S (S O)) (Init.Nat.add (S O) (S O))
             (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                (S (S O)) (S (S O)) (Init.Nat.add (S O) (S O))
                (@SHCompose Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                   (S (S O)) (S O) (Init.Nat.add (S O) (S O))
                   (@ScatH Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                      (S O) (Init.Nat.add (S O) (S O)) (S O) 
                      (S O) (h_bound_second_half (S O) (S O))
                      (@ScatH_stride1_constr (S O) (S (S O))))
                   (@liftM_HOperator Monoid_RthetaFlags (S (S O)) 
                      (S O) (@zero CarrierA CarrierAz)
                      (@HReduction (S (S O))
                         (@minmax.max CarrierA CarrierAle CarrierAledec)
                         (@zero CarrierA CarrierAz))
                      (@HReduction_HOperator (S (S O))
                         (@minmax.max CarrierA CarrierAle CarrierAledec)
                         (@abstract_algebra.sg_op_proper CarrierA CarrierAe
                            (fun x y : CarrierA =>
                             @snd CarrierA CarrierA
                               (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                            (@abstract_algebra.comsg_setoid CarrierA CarrierAe
                               (fun x y : CarrierA =>
                                @snd CarrierA CarrierA
                                  (@minmax.sort CarrierA CarrierAle CarrierAledec x y))
                               (@abstract_algebra.semilattice_sg CarrierA CarrierAe
                                  (fun x y : CarrierA =>
                                   @snd CarrierA CarrierA
                                     (@minmax.sort CarrierA CarrierAle CarrierAledec x
                                        y))
                                  (@abstract_algebra.join_semilattice CarrierA
                                     CarrierAe
                                     (fun x y : CarrierA =>
                                      @snd CarrierA CarrierA
                                        (@minmax.sort CarrierA CarrierAle CarrierAledec
                                           x y))
                                     (@abstract_algebra.lattice_join CarrierA CarrierAe
                                        (fun x y : CarrierA =>
                                         @snd CarrierA CarrierA
                                           (@minmax.sort CarrierA CarrierAle
                                              CarrierAledec x y))
                                        (@minmax.min CarrierA CarrierAle CarrierAledec)
                                        (@abstract_algebra.distr_lattice_lattice
                                           CarrierA CarrierAe
                                           (fun x y : CarrierA =>
                                            @snd CarrierA CarrierA
                                              (@minmax.sort CarrierA CarrierAle
                                                 CarrierAledec x y))
                                           (@minmax.min CarrierA CarrierAle
                                              CarrierAledec)
                                           (@minmax.DistributiveLattice_instance_0
                                              CarrierA CarrierAe CarrierAle CarrierAto
                                              CarrierAledec)))))))
                         (@zero CarrierA CarrierAz))))
                (@SHPointwise Monoid_RthetaFlags (@zero CarrierA CarrierAz) 
                   (S (S O))
                   (@IgnoreIndex CarrierA (S (S O))
                      (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                         CarrierAabs))
                   (@Reflexive_partial_app_morphism (forall _ : CarrierA, CarrierA)
                      (forall (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                         (_ : CarrierA), CarrierA)
                      (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                         (@equiv CarrierA CarrierAe))
                      (@respectful (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                         (forall _ : CarrierA, CarrierA)
                         (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@Sig_Equiv nat peano_naturals.nat_equiv
                               (fun x : nat => Peano.lt x (S (S O)))))
                         (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                            (@equiv CarrierA CarrierAe)))
                      (@IgnoreIndex CarrierA (S (S O)))
                      (@IgnoredIndex_proper CarrierA CarrierAe (S (S O)))
                      (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                         CarrierAabs)
                      (@proper_proper_proxy (forall _ : CarrierA, CarrierA)
                         (@abs CarrierA CarrierAe CarrierAle CarrierAz CarrierAneg
                            CarrierAabs)
                         (@respectful CarrierA CarrierA (@equiv CarrierA CarrierAe)
                            (@equiv CarrierA CarrierAe))
                         MDSigmaHCOLEvalSigCarrierA.abs_proper))))
             (@SumSparseEmbedding (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                (S (S O)) (Init.Nat.add (S O) (S O)) (S O)
                (fun jf : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @SafeCast (@zero CarrierA CarrierAz) (Init.Nat.add (S O) (S O)) 
                   (S O)
                   (@SHBinOp Monoid_RthetaSafeFlags (@zero CarrierA CarrierAz) 
                      (S O)
                      (@Fin1SwapIndex2 CarrierA (S (S O)) jf
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@sub CarrierA CarrierAplus CarrierAneg)))
                      (@Reflexive_partial_app_morphism
                         (forall (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (forall (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                            (_ : CarrierA) (_ : CarrierA), CarrierA)
                         (@respectful (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (@respectful (@sig nat (fun n : nat => Peano.lt n (S O)))
                            (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun n : nat => Peano.lt n (S O)))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun n : nat => Peano.lt n (S O))))
                            (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                               (@equiv CarrierA CarrierAe)
                               (@respectful CarrierA CarrierA
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv CarrierA CarrierAe))))
                         (@Fin1SwapIndex2 CarrierA (S (S O)) jf)
                         (@Reflexive_partial_app_morphism
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (forall
                               (_ : forall
                                      (_ : @sig nat
                                             (fun x : nat => Peano.lt x (S (S O))))
                                      (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@Sig_Equiv nat peano_naturals.nat_equiv
                                  (fun x : nat => Peano.lt x (S (S O)))))
                            (@respectful
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall (_ : @sig nat (fun n : nat => Peano.lt n (S O)))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@respectful
                                  (@sig nat (fun n : nat => Peano.lt n (S O)))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv (@sig nat (fun n : nat => Peano.lt n (S O)))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun n : nat => Peano.lt n (S O))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe)))))
                            (@Fin1SwapIndex2 CarrierA (S (S O)))
                            (@Fin1SwapIndex2_proper CarrierA CarrierAe (S (S O))) jf
                            (@reflexive_proper_proxy
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@Equivalence_Reflexive
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@abstract_algebra.setoid_eq
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O))))
                                     (@setoids.sig_setoid nat peano_naturals.nat_equiv
                                        (@abstract_algebra.sg_setoid nat
                                           peano_naturals.nat_equiv
                                           (@meet_is_sg_op nat
                                              (@minmax.min nat
                                                 (@le nat peano_naturals.nat_le)
                                                 (@peano_naturals.nat_le_dec)))
                                           (@abstract_algebra.comsg_setoid nat
                                              peano_naturals.nat_equiv
                                              (@meet_is_sg_op nat
                                                 (@minmax.min nat
                                                    (@le nat peano_naturals.nat_le)
                                                    (@peano_naturals.nat_le_dec)))
                                              (@abstract_algebra.semilattice_sg nat
                                                 peano_naturals.nat_equiv
                                                 (@meet_is_sg_op nat
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec)))
                                                 (@abstract_algebra.meet_semilattice
                                                    nat peano_naturals.nat_equiv
                                                    (@minmax.min nat
                                                       (@le nat peano_naturals.nat_le)
                                                       (@peano_naturals.nat_le_dec))
                                                    (@abstract_algebra.lattice_meet nat
                                                       peano_naturals.nat_equiv
                                                       (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                       (@abstract_algebra.distr_lattice_lattice
                                                          nat peano_naturals.nat_equiv
                                                          (@minmax.max nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.min nat
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@peano_naturals.nat_le_dec))
                                                          (@minmax.DistributiveLattice_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@le nat
                                                          peano_naturals.nat_le)
                                                          (@orders.le_total nat
                                                          peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          (@semirings.FullPseudoOrder_instance_0
                                                          nat peano_naturals.nat_equiv
                                                          (@strong_setoids.default_apart
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_plus
                                                          peano_naturals.nat_mult
                                                          peano_naturals.nat_0
                                                          peano_naturals.nat_1
                                                          peano_naturals.nat_le
                                                          peano_naturals.nat_lt
                                                          peano_naturals.FullPseudoSemiRingOrder_instance_0)
                                                          (@strong_setoids.default_apart_trivial
                                                          nat peano_naturals.nat_equiv)
                                                          peano_naturals.nat_dec)
                                                          (@peano_naturals.nat_le_dec))))))))
                                        (fun x : nat => Peano.lt x (S (S O)))))) jf))
                         (@IgnoreIndex2 CarrierA
                            (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                            (@sub CarrierA CarrierAplus CarrierAneg))
                         (@proper_proper_proxy
                            (forall
                               (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (_ : CarrierA) (_ : CarrierA), CarrierA)
                            (@IgnoreIndex2 CarrierA
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (@sub CarrierA CarrierAplus CarrierAneg))
                            (@respectful
                               (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@equiv (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@respectful CarrierA CarrierA
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv CarrierA CarrierAe))))
                            (@Reflexive_partial_app_morphism
                               (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (forall
                                  (_ : @sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (_ : CarrierA) (_ : CarrierA), CarrierA)
                               (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                  (@equiv CarrierA CarrierAe)
                                  (@equiv (forall _ : CarrierA, CarrierA)
                                     (@ext_equiv CarrierA CarrierAe CarrierA CarrierAe)))
                               (@respectful
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@equiv
                                     (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                     (@Sig_Equiv nat peano_naturals.nat_equiv
                                        (fun x : nat => Peano.lt x (S (S O)))))
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@respectful CarrierA CarrierA
                                        (@equiv CarrierA CarrierAe)
                                        (@equiv CarrierA CarrierAe))))
                               (@IgnoreIndex2 CarrierA
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O)))))
                               (@IgnoreIndex2_proper CarrierA CarrierAe
                                  (@sig nat (fun x : nat => Peano.lt x (S (S O))))
                                  (@Sig_Equiv nat peano_naturals.nat_equiv
                                     (fun x : nat => Peano.lt x (S (S O)))))
                               (@sub CarrierA CarrierAplus CarrierAneg)
                               (@proper_proper_proxy
                                  (forall (_ : CarrierA) (_ : CarrierA), CarrierA)
                                  (@sub CarrierA CarrierAplus CarrierAneg)
                                  (@respectful CarrierA (forall _ : CarrierA, CarrierA)
                                     (@equiv CarrierA CarrierAe)
                                     (@equiv (forall _ : CarrierA, CarrierA)
                                        (@ext_equiv CarrierA CarrierAe CarrierA
                                           CarrierAe)))
                                  MDSigmaHCOLEvalSigCarrierA.sub_proper))))))
                (fun j : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @h_index_map (S O) (S (S O))
                   (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j) 
                   (S O)
                   (ScatH_1_to_n_range_bound
                      (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j)
                      (S (S O)) (S O)
                      (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) j)))
                (@h_j_1_family_injective (S (S O)))
                (fun j : @sig nat (fun x : nat => Peano.lt x (S (S O))) =>
                 @h_index_map (S (S O)) (Init.Nat.add (S (S O)) (S (S O)))
                   (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j) 
                   (S (S O))
                   (GathH_jn_domain_bound
                      (@proj1_sig nat (fun x : nat => Peano.lt x (S (S O))) j)
                      (S (S O))
                      (@proj2_sig nat (fun x : nat => Peano.lt x (S (S O))) j)))))
          (@GathH Monoid_RthetaFlags (@zero CarrierA CarrierAz)
             (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (S (S O))))
             (Init.Nat.add (S (S O)) (S (S O))) (S O) (S O)
             (h_bound_second_half (S O) (Init.Nat.add (S (S O)) (S (S O)))))))".

vzaliva · 2019-11-27T02:37:24Z

P.S. I know these expressions are huge, but this is when you really need diff.

vzaliva · 2020-04-03T05:54:03Z

I keep encountering this issue in various situations. I have a suggestion: how about using external diff -u command to diff the expressions? Maybe we can re-use some diff-mode or similar code for showing these diffs.

cpitclaudel · 2020-04-21T18:02:53Z

Hi there. Sorry for the delay. Frustratingly, these do not trigger overflows on my machine.
We already do the diffing with diff -u; the problem comes from just locating the two strings to diff…
The solution would be to rewrite the matcher to not user regular expressions.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

company-coq-diff-unification-error: Stack overflow in regexp matcher #222

company-coq-diff-unification-error: Stack overflow in regexp matcher #222

vzaliva commented Jul 23, 2019

cpitclaudel commented Jul 24, 2019

vzaliva commented Jul 24, 2019

cpitclaudel commented Jul 24, 2019

vzaliva commented Jul 26, 2019

cpitclaudel commented Jul 26, 2019

vzaliva commented Aug 7, 2019

vzaliva commented Nov 27, 2019

vzaliva commented Nov 27, 2019

vzaliva commented Apr 3, 2020

cpitclaudel commented Apr 21, 2020

company-coq-diff-unification-error: Stack overflow in regexp matcher #222

company-coq-diff-unification-error: Stack overflow in regexp matcher #222

Comments

vzaliva commented Jul 23, 2019

cpitclaudel commented Jul 24, 2019

vzaliva commented Jul 24, 2019

cpitclaudel commented Jul 24, 2019

vzaliva commented Jul 26, 2019

cpitclaudel commented Jul 26, 2019

vzaliva commented Aug 7, 2019

vzaliva commented Nov 27, 2019

vzaliva commented Nov 27, 2019

vzaliva commented Apr 3, 2020

cpitclaudel commented Apr 21, 2020