cpitclaudel
commented
5 years ago Oh no :( Do you have an example of the input that led to that?
Open vzaliva opened 5 years ago
cpitclaudel
commented
5 years ago Oh no :( Do you have an example of the input that led to that?
vzaliva
commented
5 years ago I will try to get you one. Just a copy of *response* buffer is what you need?
cpitclaudel
commented
5 years ago Yup, that should do
vzaliva
commented
5 years ago 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
commented
5 years ago Thanks.
vzaliva
commented
5 years ago 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)))))))))".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)))))))".P.S. I know these expressions are huge, but this is when you really need diff.
vzaliva
commented
4 years ago 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
commented
4 years ago 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.
Executing
company-coq-diff-unification-errorgot the following error "Stack overflow in regexp matcher"