Semilattices and definitional duality #1166

pi8027 · 2024-02-01T12:55:31Z

Motivation for this change

This PR is the revival of #464 (also a part of #697) based on MC2.

Closes: #464

Overlay PRs

Things done/to do

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers
tried to abide by the contribution guide
profiling (before/after this PR)

Other TODOs (to be done in separate PRs)

Improve the performance of HB.saturate: HB.saturate: take a cs pattern as a filter hierarchy-builder#414
Split order.v into sub-libraries
Adapt the subType, morphism, and closedness predicate hierarchies to new structures
Fix some pointwise and lexicographic order instances so that they commute with the dual construction
Add more lemmas about complemented lattices (the CDistrLatticeTheory and CTDistrLatticeTheory sections)

Compatibility with MathComp 1.X

[ ] I added the label TODO: MC-1 port to make sure someone ports this PR to
the mathcomp-1 branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

mathcomp/ssreflect/order.v

pi8027 · 2024-02-01T13:07:58Z

mathcomp/ssreflect/order.v

+  ((x : T^d) `|^d` y) = (x `&` y).
+Proof. by []. Qed.
+
+HB.saturate.


Another bug in HB (math-comp/hierarchy-builder#257) prevents us from doing this saturation by hand (as I commented out the code doing that below). HB.saturate is a bit slow but acceptable as a workaround.

Let's just add a FIXME pointing to the HB bug and merge as is.

mathcomp/ssreflect/order.v

pi8027 · 2024-03-12T15:24:14Z

mathcomp/ssreflect/order.v

@@ -3725,10 +4258,56 @@ Arguments bigmax_eq_arg {disp T I} x j.
 Arguments eq_bigmin {disp T I x} j.
 Arguments eq_bigmax {disp T I x} j.

+(* FIXME: lemmas in the following section should hold for any porderType *)


These lemmas introduced by #738 should hold for any porderType, not orderType. cc: @proux01

It's a separate issue, let's handle that in a separate PR.

By the way, it seems to me that, except maybe the last one, these lemmas don't hold for porderType (take for instance some x not comparable with anything in s).

Right, but doesn't it make sense to reformulate (some of) the statements to be more generic? For example:

Lemma sorted_filter_gt x s : sorted <=%O s -> [seq y <- s | x < y] = drop (count (xpredC (> x)) s) s.

I propose applying the following quick fix and taking a look at it when we have more time:

Suggested change

(* FIXME: lemmas in the following section should hold for any porderType *)

(* FIXME: some lemmas in the following section should hold for any porderType *)

Right, but doesn't it make sense to reformulate (some of) the statements to be more generic?

Yes (although that would require a deprecation phase to fix the name)

pi8027 · 2024-03-12T15:34:04Z

mathcomp/ssreflect/order.v

+(* FIXME: this instance should be dualizable, but then we should not depend   *)
+(* on the subtype mechanism, because the pointwise order on seq cannot be the *)
+(* dual of itself.                                                            *)


The pointwise order on tuples and the dual construction should commute.

There doesn't seem to be a simple immediate solution, let's keep the FIXME and not wait on it to merge the current PR.

pi8027 · 2024-03-12T15:36:54Z

mathcomp/ssreflect/order.v

+(* FIXME: In order to dualize this instance, we have to dualize the           *)
+(* [POrder_isTotal] factory. However, [min] and max are not definitional dual *)
+(* (while [min x y] and [max y x] are).                                       *)


The lexicographic order on products and the dual construction should commute.

There doesn't seem to be a simple immediate solution, let's keep the FIXME and not wait on it to merge the current PR.

mathcomp/ssreflect/order.v

pi8027 · 2024-03-15T10:58:47Z

@affeldt-aist @proux01 Would you mind taking a look at the header documentation of order.v? (IIRC, Reynald was complaining about it, particularly regarding displays.)

proux01 · 2024-03-15T13:30:52Z

@pi8027 what are your plans regarding potential backward compatibility here? Will we need to impose a breaking change to the (few) users that were using displays (according to CI, deriving, maybe extructures, multinomials and analysis, maybe coqeal and apery).

pi8027 · 2024-03-15T13:35:39Z

@proux01 Implementing a compatibility layer on the users' side seems possible. See: math-comp/multinomials#88

mathcomp/ssreflect/order.v

pi8027 · 2024-03-19T14:04:23Z

What is the right way to rename a mixin and deprecate the old name? I wanted to do something like:

#[deprecated(since="mathcomp 2.3.0", note="Use BDistrLattice_hasSectionalComplement.")]
Notation hasRelativeComplement := BDistrLattice_hasSectionalComplement.

but the result is:

Error: Abbreviation is not applied enough.

proux01 · 2024-03-19T14:10:05Z

Maybe something like

math-comp/mathcomp/algebra/ssrnum.v

Lines 5934 to 5938 in cdce9e1

    
           Module RealField_isArchimedean. 
        
           #[deprecated(since="mathcomp 2.1.0", 
        
             note="NumDomain_bounded_isArchimedean.Build instead.")] 
        
           Notation Build R p := (NumDomain_bounded_isArchimedean.Build R p). 
        
           End RealField_isArchimedean.

pi8027 · 2024-03-19T14:25:12Z

Thanks, that seems to work.

pi8027 · 2024-03-19T16:34:54Z

I don't remember how to write overlays. Where is it documented?

proux01 · 2024-03-19T16:56:35Z

There is some doc there: https://github.com/math-comp/math-comp/blob/master/README-CI-Nix.md but it seems to lack the most important sentence: most of the time it's just a matter of adding a line like

multinomials.override.version = "github_login:branch";

to common-bundles in .nix/config.nix

proux01 · 2024-03-19T16:56:50Z

But I see you found it already.

These changes should not have any semantic impact.

…order.v

This commit only moves things around for clarity, it doesn't add nor remove anything.

Again this is only moving things around, not adding nor removing anything.

- Add the tDistrLatticeType structure - For any order structure (except for complemented ones), its dual exists. This is a prerequisite of definitionally involutive duals. - Add the bOrderType, tOrderType, and tbOrderType structures. Those were missing joins.

…ctures Renamed: - finLatticeType -> finTBLatticeType, - finDistrLatticeType -> finTBDistrLatticeType, - finOrderType -> finTBOrderType, - finCDistrLatticeType -> finCTBDistrLatticeType Added: - finBPorderType, - finTPorderType, - finTBPorderType, - finLatticeType (without top and bottom), - finDistrLatticeType (without top and bottom), - finOrderType (without top and bottom)

…atticeType

proux01

Thanks a lot @pi8027 for the very nice rebase!
I got a careful look and only edited a few minor details, mostly in the changelog (c.f. the diff https://github.com/math-comp/math-comp/compare/ac092f5509a0325566b795104b3c840c059cbd33..af8ec1db2fff0d8a93e2dd4e842216a56a78b5e1 )

Everyone: feel free to give a look by commit if you want, except the last commit that remains huge, all others are now reasonnably atomic.

I'll do some profiling in the coming days and I'd like to merge by the end of next week (if overlays can be merged by then). Even if there is a performance impact, the solution likely lies much more in optimizing HB itself than the current PR, so let's not delay it further.

mathcomp/ssreflect/order.v

proux01 · 2024-04-19T07:51:57Z

mathcomp/ssreflect/order.v

+  ((x : T^d) `|^d` y) = (x `&` y).
+Proof. by []. Qed.
+
+HB.saturate.


Let's just add a FIXME pointing to the HB bug and merge as is.

mathcomp/ssreflect/order.v

proux01 · 2024-04-19T07:55:05Z

mathcomp/ssreflect/order.v


-End TLatticeTheory.
+(* TODO: complete this theory module *)


Let's merge as is. This can be done in a further PR.

Adapt to math-comp/math-comp#1166

proux01 · 2024-04-20T16:20:57Z

FWIW, some more profiling. Not much to deduce, the 26% overhead seem distributed among commits, with addition of new structures and also when adding a lot of new instances (last commit).

master: 14:09.68 (1365836ko)

840.92user 8.59system 14:09.68elapsed 99%CPU (0avgtext+0avgdata 1365836maxresident)k
ssreflect/order.vo (real: 86.68, user: 86.46, sys: 0.19, mem: 1343596 ko)
algebra/ssralg.vo (real: 60.72, user: 60.50, sys: 0.20, mem: 1352224 ko)
algebra/ssrnum.vo (real: 55.74, user: 55.52, sys: 0.22, mem: 1145280 ko)
algebra/matrix.vo (real: 33.69, user: 33.52, sys: 0.16, mem: 1214320 ko)
character/mxrepresentation.vo (real: 28.36, user: 28.18, sys: 0.15, mem: 1007352 ko)
field/algebraics_fundamentals.vo (real: 25.92, user: 25.72, sys: 0.20, mem: 1365836 ko)
algebra/finalg.vo (real: 25.86, user: 25.68, sys: 0.16, mem: 903732 ko)
solvable/extremal.vo (real: 25.84, user: 25.72, sys: 0.11, mem: 858100 ko)
field/galois.vo (real: 22.13, user: 22.01, sys: 0.11, mem: 912096 ko)
field/finfield.vo (real: 20.30, user: 20.18, sys: 0.12, mem: 1068140 ko)
character/classfun.vo (real: 19.47, user: 19.26, sys: 0.20, mem: 1068728 ko)
character/character.vo (real: 19.36, user: 19.24, sys: 0.12, mem: 961972 ko)
solvable/extraspecial.vo (real: 17.54, user: 17.45, sys: 0.08, mem: 778016 ko)
field/algC.vo (real: 16.95, user: 16.78, sys: 0.16, mem: 1014204 ko)
field/fieldext.vo (real: 16.64, user: 16.51, sys: 0.13, mem: 978716 ko)
algebra/mxpoly.vo (real: 13.41, user: 13.29, sys: 0.09, mem: 767536 ko)
character/inertia.vo (real: 12.87, user: 12.79, sys: 0.08, mem: 849972 ko)
algebra/poly.vo (real: 11.81, user: 11.68, sys: 0.13, mem: 761752 ko)
solvable/burnside_app.vo (real: 11.80, user: 11.73, sys: 0.07, mem: 655648 ko)
field/closed_field.vo (real: 11.33, user: 11.16, sys: 0.16, mem: 864052 ko)
field/algnum.vo (real: 10.76, user: 10.67, sys: 0.09, mem: 830988 ko)
algebra/mxalgebra.vo (real: 10.44, user: 10.30, sys: 0.11, mem: 759000 ko)
algebra/interval.vo (real: 10.28, user: 10.12, sys: 0.16, mem: 855944 ko)
algebra/countalg.vo (real: 9.93, user: 9.81, sys: 0.11, mem: 659888 ko)
character/integral_char.vo (real: 9.72, user: 9.60, sys: 0.11, mem: 835112 ko)
algebra/vector.vo (real: 9.64, user: 9.57, sys: 0.06, mem: 806584 ko)
character/vcharacter.vo (real: 9.60, user: 9.48, sys: 0.12, mem: 826132 ko)
solvable/hall.vo (real: 9.27, user: 9.18, sys: 0.09, mem: 609616 ko)
solvable/maximal.vo (real: 9.19, user: 9.11, sys: 0.08, mem: 625432 ko)
field/qfpoly.vo (real: 9.19, user: 9.13, sys: 0.06, mem: 806976 ko)
field/falgebra.vo (real: 9.13, user: 9.01, sys: 0.11, mem: 799068 ko)
field/separable.vo (real: 8.53, user: 8.45, sys: 0.08, mem: 701540 ko)
algebra/polydiv.vo (real: 8.28, user: 8.22, sys: 0.06, mem: 603404 ko)
algebra/rat.vo (real: 8.21, user: 8.17, sys: 0.03, mem: 752256 ko)
algebra/qpoly.vo (real: 8.15, user: 8.04, sys: 0.11, mem: 759296 ko)
character/mxabelem.vo (real: 8.06, user: 7.96, sys: 0.10, mem: 687860 ko)
fingroup/gproduct.vo (real: 7.80, user: 7.74, sys: 0.06, mem: 562076 ko)
solvable/abelian.vo (real: 7.72, user: 7.65, sys: 0.07, mem: 618184 ko)
algebra/ssrint.vo (real: 7.66, user: 7.56, sys: 0.10, mem: 765412 ko)
algebra/ring_quotient.vo (real: 7.08, user: 7.01, sys: 0.07, mem: 638872 ko)
fingroup/action.vo (real: 7.01, user: 6.94, sys: 0.07, mem: 538424 ko)
algebra/intdiv.vo (real: 6.31, user: 6.22, sys: 0.09, mem: 731544 ko)
solvable/finmodule.vo (real: 5.58, user: 5.48, sys: 0.09, mem: 594564 ko)
fingroup/fingroup.vo (real: 5.11, user: 5.04, sys: 0.04, mem: 548048 ko)
solvable/alt.vo (real: 4.80, user: 4.69, sys: 0.10, mem: 567716 ko)
solvable/center.vo (real: 4.53, user: 4.47, sys: 0.06, mem: 567980 ko)
ssreflect/seq.vo (real: 4.26, user: 4.17, sys: 0.08, mem: 525016 ko)
ssreflect/bigop.vo (real: 4.22, user: 4.15, sys: 0.06, mem: 537848 ko)
fingroup/morphism.vo (real: 4.04, user: 3.98, sys: 0.03, mem: 494808 ko)
ssreflect/finset.vo (real: 4.00, user: 3.91, sys: 0.08, mem: 517784 ko)
algebra/polyXY.vo (real: 3.74, user: 3.66, sys: 0.07, mem: 635672 ko)
solvable/jordanholder.vo (real: 3.73, user: 3.61, sys: 0.10, mem: 557168 ko)
solvable/frobenius.vo (real: 3.71, user: 3.62, sys: 0.08, mem: 570456 ko)
fingroup/quotient.vo (real: 3.70, user: 3.66, sys: 0.04, mem: 485716 ko)
solvable/pgroup.vo (real: 3.64, user: 3.57, sys: 0.07, mem: 570508 ko)
algebra/zmodp.vo (real: 3.60, user: 3.52, sys: 0.08, mem: 586704 ko)
field/cyclotomic.vo (real: 3.57, user: 3.46, sys: 0.11, mem: 710088 ko)
solvable/cyclic.vo (real: 3.52, user: 3.45, sys: 0.06, mem: 567932 ko)
algebra/archimedean.vo (real: 3.49, user: 3.43, sys: 0.04, mem: 647236 ko)
ssreflect/fintype.vo (real: 3.36, user: 3.23, sys: 0.13, mem: 518144 ko)
all/all.vo (real: 3.26, user: 3.13, sys: 0.12, mem: 765260 ko)
algebra/fraction.vo (real: 3.13, user: 3.05, sys: 0.08, mem: 564164 ko)
solvable/gseries.vo (real: 2.78, user: 2.68, sys: 0.09, mem: 553356 ko)
solvable/sylow.vo (real: 2.64, user: 2.59, sys: 0.04, mem: 559380 ko)
ssreflect/prime.vo (real: 2.45, user: 2.41, sys: 0.04, mem: 471212 ko)
solvable/nilpotent.vo (real: 2.40, user: 2.37, sys: 0.02, mem: 555364 ko)
ssreflect/choice.vo (real: 2.08, user: 2.04, sys: 0.04, mem: 471744 ko)
solvable/primitive_action.vo (real: 2.07, user: 2.05, sys: 0.02, mem: 553632 ko)
ssreflect/path.vo (real: 1.93, user: 1.83, sys: 0.09, mem: 456092 ko)
algebra/all_algebra.vo (real: 1.92, user: 1.84, sys: 0.08, mem: 676404 ko)
fingroup/perm.vo (real: 1.87, user: 1.74, sys: 0.12, mem: 482484 ko)
fingroup/automorphism.vo (real: 1.86, user: 1.81, sys: 0.04, mem: 471232 ko)
solvable/gfunctor.vo (real: 1.67, user: 1.64, sys: 0.03, mem: 478780 ko)
ssreflect/fingraph.vo (real: 1.56, user: 1.42, sys: 0.14, mem: 453812 ko)
ssreflect/ssrnat.vo (real: 1.49, user: 1.44, sys: 0.05, mem: 462124 ko)
ssreflect/binomial.vo (real: 1.46, user: 1.40, sys: 0.06, mem: 472904 ko)
character/all_character.vo (real: 1.36, user: 1.27, sys: 0.09, mem: 721344 ko)
ssreflect/generic_quotient.vo (real: 1.30, user: 1.22, sys: 0.08, mem: 478400 ko)
field/all_field.vo (real: 1.29, user: 1.21, sys: 0.08, mem: 696792 ko)
ssreflect/tuple.vo (real: 1.16, user: 1.09, sys: 0.07, mem: 471564 ko)
ssreflect/all_ssreflect.vo (real: 1.16, user: 1.09, sys: 0.07, mem: 516384 ko)
ssreflect/finfun.vo (real: 1.13, user: 1.09, sys: 0.04, mem: 463056 ko)
ssreflect/eqtype.vo (real: 1.09, user: 1.01, sys: 0.08, mem: 451364 ko)
solvable/commutator.vo (real: 1.06, user: 1.02, sys: 0.04, mem: 480192 ko)
ssreflect/div.vo (real: 1.05, user: 0.97, sys: 0.08, mem: 447996 ko)
solvable/all_solvable.vo (real: 0.89, user: 0.82, sys: 0.07, mem: 609792 ko)
fingroup/presentation.vo (real: 0.54, user: 0.49, sys: 0.05, mem: 468564 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.33, sys: 0.06, mem: 448972 ko)
fingroup/all_fingroup.vo (real: 0.39, user: 0.26, sys: 0.13, mem: 464764 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.02, mem: 141928 ko)
ssreflect/ssrfun.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 111856 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 87028 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.03, sys: 0.01, mem: 74936 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.01, sys: 0.02, mem: 72232 ko)

Add subCountType and subFinType instances on copies of n.-tuple T in order.v: 14:17.41 (1376068ko)

848.50user 8.83system 14:17.41elapsed 99%CPU (0avgtext+0avgdata 1376068maxresident)k
ssreflect/order.vo (real: 86.13, user: 85.91, sys: 0.22, mem: 1303852 ko)
algebra/ssralg.vo (real: 59.20, user: 59.02, sys: 0.17, mem: 1352644 ko)
algebra/ssrnum.vo (real: 55.66, user: 55.55, sys: 0.10, mem: 1174628 ko)
algebra/matrix.vo (real: 34.81, user: 34.66, sys: 0.15, mem: 1213620 ko)
character/mxrepresentation.vo (real: 29.00, user: 28.87, sys: 0.11, mem: 1002556 ko)
algebra/finalg.vo (real: 27.02, user: 26.94, sys: 0.07, mem: 902548 ko)
solvable/extremal.vo (real: 25.84, user: 25.67, sys: 0.16, mem: 856096 ko)
field/algebraics_fundamentals.vo (real: 25.84, user: 25.51, sys: 0.30, mem: 1376068 ko)
field/galois.vo (real: 22.12, user: 21.98, sys: 0.14, mem: 911208 ko)
field/finfield.vo (real: 20.04, user: 19.85, sys: 0.18, mem: 1065984 ko)
character/classfun.vo (real: 20.01, user: 19.82, sys: 0.19, mem: 1067972 ko)
character/character.vo (real: 18.41, user: 18.33, sys: 0.07, mem: 957376 ko)
solvable/extraspecial.vo (real: 17.53, user: 17.38, sys: 0.14, mem: 780084 ko)
field/algC.vo (real: 17.33, user: 17.20, sys: 0.13, mem: 1015476 ko)
field/fieldext.vo (real: 17.16, user: 17.10, sys: 0.06, mem: 976764 ko)
algebra/mxpoly.vo (real: 14.08, user: 13.99, sys: 0.09, mem: 768688 ko)
character/inertia.vo (real: 12.91, user: 12.79, sys: 0.12, mem: 850020 ko)
solvable/burnside_app.vo (real: 11.70, user: 11.58, sys: 0.11, mem: 655668 ko)
field/closed_field.vo (real: 11.67, user: 11.52, sys: 0.15, mem: 862112 ko)
algebra/poly.vo (real: 11.52, user: 11.45, sys: 0.05, mem: 761848 ko)
algebra/mxalgebra.vo (real: 11.18, user: 11.05, sys: 0.13, mem: 758520 ko)
algebra/interval.vo (real: 10.79, user: 10.69, sys: 0.10, mem: 854860 ko)
field/algnum.vo (real: 10.58, user: 10.47, sys: 0.11, mem: 833556 ko)
algebra/vector.vo (real: 10.05, user: 9.90, sys: 0.14, mem: 808672 ko)
character/vcharacter.vo (real: 9.95, user: 9.85, sys: 0.10, mem: 827120 ko)
algebra/countalg.vo (real: 9.93, user: 9.84, sys: 0.09, mem: 661232 ko)
character/integral_char.vo (real: 9.72, user: 9.62, sys: 0.10, mem: 833784 ko)
field/falgebra.vo (real: 9.62, user: 9.42, sys: 0.20, mem: 797616 ko)
field/qfpoly.vo (real: 9.16, user: 9.03, sys: 0.10, mem: 809280 ko)
solvable/hall.vo (real: 9.12, user: 9.03, sys: 0.07, mem: 609768 ko)
solvable/maximal.vo (real: 8.76, user: 8.66, sys: 0.10, mem: 625260 ko)
algebra/polydiv.vo (real: 8.71, user: 8.62, sys: 0.09, mem: 603308 ko)
fingroup/gproduct.vo (real: 8.69, user: 8.64, sys: 0.04, mem: 562104 ko)
algebra/rat.vo (real: 8.61, user: 8.54, sys: 0.07, mem: 753604 ko)
field/separable.vo (real: 8.57, user: 8.44, sys: 0.13, mem: 699928 ko)
algebra/ssrint.vo (real: 8.57, user: 8.36, sys: 0.20, mem: 765932 ko)
algebra/qpoly.vo (real: 8.43, user: 8.32, sys: 0.11, mem: 759356 ko)
character/mxabelem.vo (real: 8.06, user: 7.91, sys: 0.13, mem: 685932 ko)
algebra/ring_quotient.vo (real: 7.73, user: 7.65, sys: 0.08, mem: 639152 ko)
solvable/abelian.vo (real: 7.71, user: 7.63, sys: 0.08, mem: 618856 ko)
fingroup/action.vo (real: 6.63, user: 6.56, sys: 0.06, mem: 538340 ko)
algebra/intdiv.vo (real: 6.54, user: 6.42, sys: 0.10, mem: 731932 ko)
fingroup/fingroup.vo (real: 5.12, user: 5.06, sys: 0.06, mem: 552380 ko)
solvable/finmodule.vo (real: 5.02, user: 4.92, sys: 0.10, mem: 591008 ko)
solvable/alt.vo (real: 5.01, user: 4.91, sys: 0.10, mem: 569912 ko)
solvable/center.vo (real: 4.74, user: 4.66, sys: 0.08, mem: 568172 ko)
fingroup/morphism.vo (real: 4.46, user: 4.40, sys: 0.06, mem: 489816 ko)
ssreflect/seq.vo (real: 4.19, user: 4.14, sys: 0.05, mem: 524476 ko)
ssreflect/bigop.vo (real: 4.14, user: 4.03, sys: 0.11, mem: 538268 ko)
solvable/pgroup.vo (real: 3.95, user: 3.85, sys: 0.10, mem: 570328 ko)
algebra/polyXY.vo (real: 3.95, user: 3.89, sys: 0.04, mem: 635160 ko)
ssreflect/finset.vo (real: 3.89, user: 3.80, sys: 0.09, mem: 515296 ko)
algebra/zmodp.vo (real: 3.83, user: 3.72, sys: 0.10, mem: 587512 ko)
solvable/cyclic.vo (real: 3.70, user: 3.64, sys: 0.05, mem: 568604 ko)
solvable/jordanholder.vo (real: 3.68, user: 3.62, sys: 0.06, mem: 556812 ko)
solvable/frobenius.vo (real: 3.66, user: 3.60, sys: 0.06, mem: 570376 ko)
field/cyclotomic.vo (real: 3.66, user: 3.53, sys: 0.12, mem: 709736 ko)
algebra/archimedean.vo (real: 3.64, user: 3.54, sys: 0.09, mem: 647284 ko)
ssreflect/fintype.vo (real: 3.33, user: 3.23, sys: 0.10, mem: 518960 ko)
fingroup/quotient.vo (real: 3.30, user: 3.25, sys: 0.04, mem: 486052 ko)
algebra/fraction.vo (real: 3.30, user: 3.20, sys: 0.10, mem: 560532 ko)
all/all.vo (real: 3.20, user: 3.11, sys: 0.09, mem: 764712 ko)
solvable/gseries.vo (real: 2.96, user: 2.91, sys: 0.05, mem: 554400 ko)
solvable/sylow.vo (real: 2.76, user: 2.67, sys: 0.09, mem: 558056 ko)
solvable/nilpotent.vo (real: 2.55, user: 2.48, sys: 0.07, mem: 556056 ko)
ssreflect/prime.vo (real: 2.40, user: 2.37, sys: 0.03, mem: 472652 ko)
ssreflect/choice.vo (real: 2.03, user: 2.01, sys: 0.02, mem: 472876 ko)
fingroup/perm.vo (real: 1.98, user: 1.92, sys: 0.06, mem: 483156 ko)
fingroup/automorphism.vo (real: 1.96, user: 1.85, sys: 0.10, mem: 469468 ko)
algebra/all_algebra.vo (real: 1.94, user: 1.86, sys: 0.08, mem: 674764 ko)
ssreflect/path.vo (real: 1.88, user: 1.78, sys: 0.10, mem: 455600 ko)
solvable/gfunctor.vo (real: 1.78, user: 1.73, sys: 0.05, mem: 480088 ko)
solvable/primitive_action.vo (real: 1.65, user: 1.59, sys: 0.06, mem: 553724 ko)
ssreflect/fingraph.vo (real: 1.48, user: 1.37, sys: 0.10, mem: 454872 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.40, sys: 0.04, mem: 461556 ko)
ssreflect/binomial.vo (real: 1.42, user: 1.36, sys: 0.06, mem: 472696 ko)
ssreflect/generic_quotient.vo (real: 1.40, user: 1.37, sys: 0.03, mem: 476800 ko)
character/all_character.vo (real: 1.36, user: 1.27, sys: 0.09, mem: 721776 ko)
field/all_field.vo (real: 1.24, user: 1.14, sys: 0.10, mem: 697456 ko)
ssreflect/all_ssreflect.vo (real: 1.20, user: 1.14, sys: 0.05, mem: 517524 ko)
solvable/commutator.vo (real: 1.16, user: 1.10, sys: 0.06, mem: 479200 ko)
ssreflect/tuple.vo (real: 1.15, user: 1.06, sys: 0.08, mem: 473096 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.05, sys: 0.05, mem: 462728 ko)
ssreflect/eqtype.vo (real: 1.06, user: 1.01, sys: 0.05, mem: 449804 ko)
ssreflect/div.vo (real: 1.02, user: 1.00, sys: 0.02, mem: 447784 ko)
solvable/all_solvable.vo (real: 0.88, user: 0.83, sys: 0.04, mem: 609436 ko)
fingroup/presentation.vo (real: 0.54, user: 0.48, sys: 0.06, mem: 467900 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.37, sys: 0.02, mem: 448860 ko)
fingroup/all_fingroup.vo (real: 0.39, user: 0.24, sys: 0.15, mem: 465316 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.01, mem: 142060 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 113008 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 86328 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 74752 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 72424 ko)

Make the order hierarchy symmetric w.r.t. dual: 14:26.11 (1368972ko)

857.16user 8.86system 14:26.11elapsed 99%CPU (0avgtext+0avgdata 1368972maxresident)k
ssreflect/order.vo (real: 97.39, user: 97.21, sys: 0.16, mem: 1335112 ko)
algebra/ssralg.vo (real: 59.16, user: 58.93, sys: 0.23, mem: 1353428 ko)
algebra/ssrnum.vo (real: 56.76, user: 56.55, sys: 0.20, mem: 1164020 ko)
algebra/matrix.vo (real: 33.87, user: 33.67, sys: 0.19, mem: 1231144 ko)
character/mxrepresentation.vo (real: 28.07, user: 28.00, sys: 0.06, mem: 1006348 ko)
field/algebraics_fundamentals.vo (real: 26.13, user: 25.89, sys: 0.23, mem: 1368972 ko)
solvable/extremal.vo (real: 25.75, user: 25.61, sys: 0.14, mem: 858084 ko)
algebra/finalg.vo (real: 25.70, user: 25.55, sys: 0.13, mem: 901480 ko)
field/galois.vo (real: 22.17, user: 22.12, sys: 0.04, mem: 927288 ko)
field/finfield.vo (real: 20.48, user: 20.31, sys: 0.17, mem: 1027396 ko)
character/character.vo (real: 20.00, user: 19.88, sys: 0.11, mem: 966064 ko)
character/classfun.vo (real: 19.55, user: 19.37, sys: 0.17, mem: 1078428 ko)
field/algC.vo (real: 17.58, user: 17.41, sys: 0.17, mem: 1032176 ko)
solvable/extraspecial.vo (real: 17.46, user: 17.32, sys: 0.12, mem: 777896 ko)
field/fieldext.vo (real: 17.15, user: 17.06, sys: 0.09, mem: 970872 ko)
algebra/mxpoly.vo (real: 13.37, user: 13.28, sys: 0.07, mem: 765420 ko)
character/inertia.vo (real: 12.84, user: 12.72, sys: 0.11, mem: 855116 ko)
solvable/burnside_app.vo (real: 11.88, user: 11.76, sys: 0.12, mem: 657644 ko)
field/closed_field.vo (real: 11.78, user: 11.65, sys: 0.12, mem: 880680 ko)
algebra/poly.vo (real: 11.61, user: 11.53, sys: 0.08, mem: 762936 ko)
algebra/interval.vo (real: 11.38, user: 11.27, sys: 0.08, mem: 867056 ko)
field/algnum.vo (real: 10.85, user: 10.70, sys: 0.14, mem: 839016 ko)
algebra/mxalgebra.vo (real: 10.45, user: 10.39, sys: 0.04, mem: 771192 ko)
algebra/countalg.vo (real: 9.91, user: 9.82, sys: 0.08, mem: 661044 ko)
algebra/vector.vo (real: 9.87, user: 9.80, sys: 0.06, mem: 810488 ko)
character/integral_char.vo (real: 9.69, user: 9.60, sys: 0.09, mem: 833744 ko)
field/falgebra.vo (real: 9.59, user: 9.47, sys: 0.11, mem: 786420 ko)
character/vcharacter.vo (real: 9.58, user: 9.41, sys: 0.16, mem: 827984 ko)
field/qfpoly.vo (real: 9.42, user: 9.32, sys: 0.10, mem: 803088 ko)
solvable/hall.vo (real: 9.21, user: 9.12, sys: 0.07, mem: 609844 ko)
fingroup/gproduct.vo (real: 8.90, user: 8.80, sys: 0.09, mem: 562160 ko)
solvable/maximal.vo (real: 8.85, user: 8.79, sys: 0.06, mem: 623900 ko)
algebra/rat.vo (real: 8.79, user: 8.68, sys: 0.10, mem: 764840 ko)
field/separable.vo (real: 8.62, user: 8.52, sys: 0.07, mem: 699784 ko)
algebra/qpoly.vo (real: 8.38, user: 8.29, sys: 0.09, mem: 754672 ko)
algebra/polydiv.vo (real: 8.24, user: 8.11, sys: 0.12, mem: 603680 ko)
solvable/abelian.vo (real: 8.21, user: 8.11, sys: 0.10, mem: 618664 ko)
character/mxabelem.vo (real: 8.09, user: 7.96, sys: 0.13, mem: 692356 ko)
algebra/ssrint.vo (real: 8.02, user: 7.94, sys: 0.08, mem: 754520 ko)
algebra/ring_quotient.vo (real: 7.63, user: 7.55, sys: 0.08, mem: 639672 ko)
algebra/intdiv.vo (real: 6.48, user: 6.38, sys: 0.10, mem: 732072 ko)
fingroup/action.vo (real: 6.06, user: 6.02, sys: 0.04, mem: 538296 ko)
fingroup/fingroup.vo (real: 5.08, user: 5.01, sys: 0.07, mem: 550540 ko)
solvable/finmodule.vo (real: 4.90, user: 4.85, sys: 0.05, mem: 594560 ko)
solvable/center.vo (real: 4.70, user: 4.62, sys: 0.08, mem: 566040 ko)
solvable/alt.vo (real: 4.66, user: 4.61, sys: 0.05, mem: 569216 ko)
ssreflect/seq.vo (real: 4.34, user: 4.24, sys: 0.10, mem: 524600 ko)
ssreflect/bigop.vo (real: 4.14, user: 4.07, sys: 0.06, mem: 539052 ko)
fingroup/morphism.vo (real: 4.01, user: 3.93, sys: 0.08, mem: 490436 ko)
ssreflect/finset.vo (real: 3.89, user: 3.82, sys: 0.07, mem: 514660 ko)
solvable/pgroup.vo (real: 3.81, user: 3.69, sys: 0.11, mem: 569612 ko)
algebra/polyXY.vo (real: 3.79, user: 3.71, sys: 0.08, mem: 632888 ko)
algebra/archimedean.vo (real: 3.74, user: 3.66, sys: 0.08, mem: 648792 ko)
solvable/jordanholder.vo (real: 3.69, user: 3.59, sys: 0.09, mem: 557364 ko)
solvable/cyclic.vo (real: 3.69, user: 3.60, sys: 0.08, mem: 569500 ko)
solvable/frobenius.vo (real: 3.63, user: 3.53, sys: 0.09, mem: 570260 ko)
algebra/zmodp.vo (real: 3.60, user: 3.53, sys: 0.07, mem: 587420 ko)
field/cyclotomic.vo (real: 3.38, user: 3.30, sys: 0.07, mem: 711936 ko)
all/all.vo (real: 3.38, user: 3.31, sys: 0.07, mem: 767356 ko)
ssreflect/fintype.vo (real: 3.32, user: 3.23, sys: 0.09, mem: 518668 ko)
algebra/fraction.vo (real: 3.30, user: 3.26, sys: 0.04, mem: 560552 ko)
fingroup/quotient.vo (real: 3.17, user: 3.07, sys: 0.09, mem: 485288 ko)
solvable/gseries.vo (real: 2.95, user: 2.87, sys: 0.07, mem: 557700 ko)
solvable/sylow.vo (real: 2.76, user: 2.68, sys: 0.08, mem: 560436 ko)
solvable/nilpotent.vo (real: 2.57, user: 2.49, sys: 0.08, mem: 555668 ko)
ssreflect/prime.vo (real: 2.41, user: 2.32, sys: 0.08, mem: 470536 ko)
ssreflect/choice.vo (real: 2.05, user: 1.96, sys: 0.08, mem: 471548 ko)
solvable/primitive_action.vo (real: 1.94, user: 1.84, sys: 0.10, mem: 553644 ko)
ssreflect/path.vo (real: 1.89, user: 1.86, sys: 0.03, mem: 459556 ko)
fingroup/perm.vo (real: 1.89, user: 1.79, sys: 0.10, mem: 481960 ko)
algebra/all_algebra.vo (real: 1.88, user: 1.78, sys: 0.10, mem: 676012 ko)
fingroup/automorphism.vo (real: 1.85, user: 1.76, sys: 0.09, mem: 471424 ko)
solvable/gfunctor.vo (real: 1.80, user: 1.73, sys: 0.07, mem: 479712 ko)
ssreflect/ssrnat.vo (real: 1.53, user: 1.46, sys: 0.07, mem: 464744 ko)
ssreflect/fingraph.vo (real: 1.49, user: 1.41, sys: 0.07, mem: 455056 ko)
ssreflect/generic_quotient.vo (real: 1.44, user: 1.37, sys: 0.06, mem: 477012 ko)
ssreflect/binomial.vo (real: 1.42, user: 1.36, sys: 0.06, mem: 468340 ko)
character/all_character.vo (real: 1.37, user: 1.25, sys: 0.12, mem: 720024 ko)
field/all_field.vo (real: 1.36, user: 1.26, sys: 0.09, mem: 705072 ko)
ssreflect/all_ssreflect.vo (real: 1.21, user: 1.12, sys: 0.09, mem: 521784 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.11, sys: 0.03, mem: 473316 ko)
solvable/commutator.vo (real: 1.13, user: 1.06, sys: 0.06, mem: 479576 ko)
ssreflect/eqtype.vo (real: 1.11, user: 1.01, sys: 0.10, mem: 449964 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.08, sys: 0.02, mem: 462796 ko)
ssreflect/div.vo (real: 1.04, user: 0.99, sys: 0.05, mem: 447456 ko)
solvable/all_solvable.vo (real: 0.91, user: 0.80, sys: 0.10, mem: 604824 ko)
fingroup/presentation.vo (real: 0.56, user: 0.50, sys: 0.06, mem: 467332 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 448612 ko)
fingroup/all_fingroup.vo (real: 0.37, user: 0.29, sys: 0.08, mem: 465240 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.02, mem: 140752 ko)
ssreflect/ssrmatching.vo (real: 0.06, user: 0.03, sys: 0.03, mem: 72896 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.02, sys: 0.04, mem: 111704 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.01, sys: 0.04, mem: 85672 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 75592 ko)

Add missing top/bottom variants to the hierarchy of finite order structures: 14:42.53 (1467572ko)

873.18user 9.22system 14:42.53elapsed 99%CPU (0avgtext+0avgdata 1467572maxresident)k
ssreflect/order.vo (real: 108.68, user: 108.45, sys: 0.22, mem: 1467572 ko)
algebra/ssrnum.vo (real: 59.22, user: 59.01, sys: 0.20, mem: 1181244 ko)
algebra/ssralg.vo (real: 59.21, user: 59.00, sys: 0.19, mem: 1353008 ko)
algebra/matrix.vo (real: 34.78, user: 34.53, sys: 0.24, mem: 1222556 ko)
character/mxrepresentation.vo (real: 28.52, user: 28.35, sys: 0.16, mem: 1017508 ko)
field/algebraics_fundamentals.vo (real: 26.33, user: 26.16, sys: 0.17, mem: 1401440 ko)
solvable/extremal.vo (real: 25.87, user: 25.73, sys: 0.13, mem: 858588 ko)
algebra/finalg.vo (real: 25.67, user: 25.53, sys: 0.13, mem: 901264 ko)
field/galois.vo (real: 22.22, user: 22.11, sys: 0.09, mem: 905120 ko)
field/finfield.vo (real: 20.34, user: 20.11, sys: 0.23, mem: 1048876 ko)
character/classfun.vo (real: 19.89, user: 19.66, sys: 0.20, mem: 1081632 ko)
character/character.vo (real: 19.27, user: 19.10, sys: 0.14, mem: 977764 ko)
field/algC.vo (real: 17.87, user: 17.74, sys: 0.13, mem: 1035696 ko)
solvable/extraspecial.vo (real: 17.54, user: 17.36, sys: 0.15, mem: 782708 ko)
field/fieldext.vo (real: 17.47, user: 17.25, sys: 0.20, mem: 1008028 ko)
algebra/mxpoly.vo (real: 13.32, user: 13.21, sys: 0.11, mem: 774300 ko)
character/inertia.vo (real: 12.99, user: 12.89, sys: 0.09, mem: 855568 ko)
algebra/interval.vo (real: 12.11, user: 11.95, sys: 0.15, mem: 891556 ko)
solvable/burnside_app.vo (real: 11.68, user: 11.57, sys: 0.10, mem: 657956 ko)
field/closed_field.vo (real: 11.58, user: 11.46, sys: 0.12, mem: 916084 ko)
algebra/poly.vo (real: 11.53, user: 11.46, sys: 0.07, mem: 765928 ko)
field/algnum.vo (real: 10.69, user: 10.56, sys: 0.13, mem: 843120 ko)
algebra/mxalgebra.vo (real: 10.55, user: 10.48, sys: 0.07, mem: 773000 ko)
algebra/countalg.vo (real: 9.94, user: 9.87, sys: 0.05, mem: 659928 ko)
character/integral_char.vo (real: 9.82, user: 9.66, sys: 0.15, mem: 838684 ko)
algebra/vector.vo (real: 9.72, user: 9.63, sys: 0.08, mem: 789676 ko)
character/vcharacter.vo (real: 9.65, user: 9.55, sys: 0.10, mem: 833832 ko)
field/falgebra.vo (real: 9.58, user: 9.43, sys: 0.14, mem: 794956 ko)
field/qfpoly.vo (real: 9.23, user: 9.10, sys: 0.11, mem: 811660 ko)
solvable/hall.vo (real: 9.15, user: 9.08, sys: 0.06, mem: 609600 ko)
algebra/rat.vo (real: 8.89, user: 8.79, sys: 0.09, mem: 776872 ko)
solvable/maximal.vo (real: 8.87, user: 8.78, sys: 0.08, mem: 624672 ko)
fingroup/gproduct.vo (real: 8.63, user: 8.56, sys: 0.07, mem: 562364 ko)
field/separable.vo (real: 8.56, user: 8.46, sys: 0.10, mem: 704220 ko)
solvable/abelian.vo (real: 8.45, user: 8.36, sys: 0.09, mem: 621608 ko)
algebra/polydiv.vo (real: 8.26, user: 8.21, sys: 0.05, mem: 607696 ko)
character/mxabelem.vo (real: 8.07, user: 7.96, sys: 0.11, mem: 692820 ko)
algebra/qpoly.vo (real: 8.07, user: 7.98, sys: 0.08, mem: 761616 ko)
algebra/ring_quotient.vo (real: 8.06, user: 7.95, sys: 0.11, mem: 639696 ko)
algebra/ssrint.vo (real: 7.96, user: 7.86, sys: 0.09, mem: 771892 ko)
algebra/intdiv.vo (real: 6.74, user: 6.64, sys: 0.09, mem: 735004 ko)
fingroup/action.vo (real: 6.08, user: 6.01, sys: 0.07, mem: 537104 ko)
fingroup/fingroup.vo (real: 5.17, user: 5.07, sys: 0.10, mem: 547608 ko)
solvable/alt.vo (real: 5.10, user: 4.94, sys: 0.16, mem: 569036 ko)
solvable/finmodule.vo (real: 4.88, user: 4.81, sys: 0.07, mem: 589624 ko)
solvable/center.vo (real: 4.72, user: 4.62, sys: 0.10, mem: 566612 ko)
ssreflect/bigop.vo (real: 4.14, user: 4.05, sys: 0.09, mem: 539756 ko)
ssreflect/seq.vo (real: 4.13, user: 4.05, sys: 0.08, mem: 525540 ko)
fingroup/morphism.vo (real: 4.03, user: 3.98, sys: 0.05, mem: 494668 ko)
solvable/frobenius.vo (real: 3.99, user: 3.94, sys: 0.04, mem: 569856 ko)
ssreflect/finset.vo (real: 3.89, user: 3.80, sys: 0.08, mem: 517880 ko)
solvable/pgroup.vo (real: 3.82, user: 3.72, sys: 0.10, mem: 569436 ko)
algebra/archimedean.vo (real: 3.77, user: 3.63, sys: 0.12, mem: 656840 ko)
algebra/polyXY.vo (real: 3.76, user: 3.69, sys: 0.06, mem: 637760 ko)
solvable/cyclic.vo (real: 3.67, user: 3.59, sys: 0.07, mem: 568064 ko)
solvable/jordanholder.vo (real: 3.63, user: 3.54, sys: 0.09, mem: 559172 ko)
algebra/zmodp.vo (real: 3.62, user: 3.58, sys: 0.04, mem: 587984 ko)
field/cyclotomic.vo (real: 3.46, user: 3.33, sys: 0.13, mem: 716520 ko)
ssreflect/fintype.vo (real: 3.33, user: 3.20, sys: 0.12, mem: 517856 ko)
all/all.vo (real: 3.27, user: 3.16, sys: 0.11, mem: 779244 ko)
algebra/fraction.vo (real: 3.22, user: 3.09, sys: 0.13, mem: 561368 ko)
fingroup/quotient.vo (real: 3.14, user: 3.08, sys: 0.06, mem: 484972 ko)
solvable/gseries.vo (real: 2.98, user: 2.92, sys: 0.05, mem: 553048 ko)
solvable/sylow.vo (real: 2.79, user: 2.68, sys: 0.11, mem: 559904 ko)
solvable/nilpotent.vo (real: 2.50, user: 2.46, sys: 0.04, mem: 556240 ko)
ssreflect/prime.vo (real: 2.40, user: 2.35, sys: 0.04, mem: 471156 ko)
ssreflect/choice.vo (real: 2.03, user: 1.96, sys: 0.06, mem: 471988 ko)
fingroup/automorphism.vo (real: 1.91, user: 1.81, sys: 0.10, mem: 469888 ko)
ssreflect/path.vo (real: 1.90, user: 1.85, sys: 0.04, mem: 455588 ko)
fingroup/perm.vo (real: 1.88, user: 1.84, sys: 0.04, mem: 482552 ko)
algebra/all_algebra.vo (real: 1.86, user: 1.79, sys: 0.07, mem: 684956 ko)
solvable/primitive_action.vo (real: 1.83, user: 1.76, sys: 0.07, mem: 554108 ko)
solvable/gfunctor.vo (real: 1.83, user: 1.79, sys: 0.04, mem: 478316 ko)
ssreflect/generic_quotient.vo (real: 1.48, user: 1.42, sys: 0.04, mem: 475856 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.37, sys: 0.06, mem: 466976 ko)
ssreflect/binomial.vo (real: 1.43, user: 1.39, sys: 0.03, mem: 468400 ko)
ssreflect/fingraph.vo (real: 1.42, user: 1.34, sys: 0.08, mem: 453536 ko)
character/all_character.vo (real: 1.39, user: 1.33, sys: 0.06, mem: 721308 ko)
field/all_field.vo (real: 1.29, user: 1.23, sys: 0.05, mem: 707100 ko)
ssreflect/all_ssreflect.vo (real: 1.21, user: 1.12, sys: 0.08, mem: 523624 ko)
solvable/commutator.vo (real: 1.15, user: 1.10, sys: 0.05, mem: 484336 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.08, sys: 0.06, mem: 473124 ko)
ssreflect/finfun.vo (real: 1.10, user: 0.99, sys: 0.11, mem: 468084 ko)
ssreflect/eqtype.vo (real: 1.06, user: 1.03, sys: 0.03, mem: 449316 ko)
ssreflect/div.vo (real: 1.03, user: 0.97, sys: 0.05, mem: 446456 ko)
solvable/all_solvable.vo (real: 0.93, user: 0.86, sys: 0.06, mem: 607204 ko)
fingroup/presentation.vo (real: 0.59, user: 0.48, sys: 0.08, mem: 467736 ko)
fingroup/all_fingroup.vo (real: 0.43, user: 0.28, sys: 0.14, mem: 464572 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.37, sys: 0.03, mem: 448504 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 140012 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 112064 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 86292 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 76060 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.00, sys: 0.03, mem: 73484 ko)

Generalize some order lemmas to bPOrderType, tPOrderType, and tDistrLatticeType: 14:32.08 (1472992ko)

863.03user 8.93system 14:32.08elapsed 99%CPU (0avgtext+0avgdata 1472992maxresident)k
ssreflect/order.vo (real: 108.76, user: 108.54, sys: 0.22, mem: 1472992 ko)
algebra/ssralg.vo (real: 59.46, user: 59.16, sys: 0.27, mem: 1353384 ko)
algebra/ssrnum.vo (real: 59.40, user: 59.27, sys: 0.11, mem: 1208888 ko)
algebra/matrix.vo (real: 34.92, user: 34.67, sys: 0.24, mem: 1237708 ko)
character/mxrepresentation.vo (real: 28.32, user: 28.12, sys: 0.17, mem: 1011760 ko)
algebra/finalg.vo (real: 25.92, user: 25.81, sys: 0.10, mem: 905700 ko)
solvable/extremal.vo (real: 25.56, user: 25.48, sys: 0.08, mem: 860064 ko)
field/algebraics_fundamentals.vo (real: 25.12, user: 24.88, sys: 0.23, mem: 1379092 ko)
field/galois.vo (real: 21.10, user: 20.93, sys: 0.17, mem: 903336 ko)
field/finfield.vo (real: 20.39, user: 20.19, sys: 0.19, mem: 1046096 ko)
character/classfun.vo (real: 19.84, user: 19.69, sys: 0.15, mem: 1087372 ko)
character/character.vo (real: 19.84, user: 19.71, sys: 0.13, mem: 972328 ko)
solvable/extraspecial.vo (real: 17.60, user: 17.50, sys: 0.10, mem: 780524 ko)
field/algC.vo (real: 17.24, user: 17.06, sys: 0.18, mem: 1058008 ko)
field/fieldext.vo (real: 16.69, user: 16.61, sys: 0.08, mem: 1010064 ko)
algebra/mxpoly.vo (real: 13.59, user: 13.51, sys: 0.08, mem: 770580 ko)
character/inertia.vo (real: 12.77, user: 12.59, sys: 0.17, mem: 864896 ko)
algebra/poly.vo (real: 11.84, user: 11.76, sys: 0.08, mem: 765760 ko)
solvable/burnside_app.vo (real: 11.41, user: 11.33, sys: 0.08, mem: 654616 ko)
field/closed_field.vo (real: 11.28, user: 11.16, sys: 0.11, mem: 885236 ko)
algebra/interval.vo (real: 11.09, user: 10.97, sys: 0.10, mem: 893308 ko)
algebra/mxalgebra.vo (real: 10.59, user: 10.47, sys: 0.12, mem: 770744 ko)
field/algnum.vo (real: 10.44, user: 10.33, sys: 0.11, mem: 841876 ko)
algebra/countalg.vo (real: 9.94, user: 9.83, sys: 0.10, mem: 660520 ko)
algebra/vector.vo (real: 9.74, user: 9.62, sys: 0.11, mem: 803032 ko)
character/integral_char.vo (real: 9.59, user: 9.51, sys: 0.08, mem: 840200 ko)
solvable/hall.vo (real: 9.47, user: 9.38, sys: 0.09, mem: 609728 ko)
character/vcharacter.vo (real: 9.47, user: 9.29, sys: 0.16, mem: 832132 ko)
field/qfpoly.vo (real: 9.23, user: 9.12, sys: 0.11, mem: 811660 ko)
field/falgebra.vo (real: 9.22, user: 9.14, sys: 0.07, mem: 789548 ko)
solvable/maximal.vo (real: 8.85, user: 8.70, sys: 0.14, mem: 624512 ko)
algebra/rat.vo (real: 8.55, user: 8.42, sys: 0.12, mem: 779972 ko)
algebra/polydiv.vo (real: 8.28, user: 8.13, sys: 0.15, mem: 603060 ko)
field/separable.vo (real: 8.21, user: 8.14, sys: 0.06, mem: 703312 ko)
algebra/qpoly.vo (real: 8.15, user: 8.03, sys: 0.11, mem: 761676 ko)
solvable/abelian.vo (real: 8.05, user: 8.01, sys: 0.04, mem: 618180 ko)
fingroup/gproduct.vo (real: 8.04, user: 7.96, sys: 0.07, mem: 562256 ko)
algebra/ssrint.vo (real: 7.93, user: 7.81, sys: 0.11, mem: 767056 ko)
character/mxabelem.vo (real: 7.88, user: 7.79, sys: 0.09, mem: 694656 ko)
algebra/ring_quotient.vo (real: 7.11, user: 7.03, sys: 0.06, mem: 640488 ko)
algebra/intdiv.vo (real: 6.24, user: 6.19, sys: 0.05, mem: 739780 ko)
fingroup/action.vo (real: 6.07, user: 6.01, sys: 0.06, mem: 537692 ko)
fingroup/fingroup.vo (real: 5.06, user: 4.89, sys: 0.16, mem: 548440 ko)
solvable/alt.vo (real: 4.90, user: 4.79, sys: 0.10, mem: 569976 ko)
solvable/finmodule.vo (real: 4.85, user: 4.78, sys: 0.07, mem: 589964 ko)
solvable/center.vo (real: 4.50, user: 4.42, sys: 0.08, mem: 566016 ko)
ssreflect/bigop.vo (real: 4.15, user: 4.05, sys: 0.10, mem: 539044 ko)
ssreflect/seq.vo (real: 4.12, user: 4.07, sys: 0.05, mem: 524556 ko)
fingroup/morphism.vo (real: 4.08, user: 4.05, sys: 0.03, mem: 490020 ko)
ssreflect/finset.vo (real: 3.91, user: 3.83, sys: 0.07, mem: 518000 ko)
algebra/polyXY.vo (real: 3.86, user: 3.78, sys: 0.07, mem: 639140 ko)
solvable/frobenius.vo (real: 3.67, user: 3.61, sys: 0.06, mem: 568736 ko)
solvable/pgroup.vo (real: 3.65, user: 3.58, sys: 0.05, mem: 569360 ko)
solvable/jordanholder.vo (real: 3.64, user: 3.59, sys: 0.05, mem: 559196 ko)
algebra/zmodp.vo (real: 3.62, user: 3.54, sys: 0.08, mem: 590992 ko)
algebra/archimedean.vo (real: 3.62, user: 3.57, sys: 0.05, mem: 657492 ko)
solvable/cyclic.vo (real: 3.51, user: 3.40, sys: 0.10, mem: 570724 ko)
all/all.vo (real: 3.35, user: 3.21, sys: 0.14, mem: 777760 ko)
ssreflect/fintype.vo (real: 3.32, user: 3.23, sys: 0.09, mem: 517968 ko)
field/cyclotomic.vo (real: 3.30, user: 3.14, sys: 0.13, mem: 717120 ko)
fingroup/quotient.vo (real: 3.14, user: 3.10, sys: 0.04, mem: 485028 ko)
algebra/fraction.vo (real: 3.14, user: 3.04, sys: 0.10, mem: 561052 ko)
solvable/gseries.vo (real: 2.79, user: 2.73, sys: 0.05, mem: 553196 ko)
solvable/sylow.vo (real: 2.64, user: 2.58, sys: 0.06, mem: 557576 ko)
ssreflect/prime.vo (real: 2.40, user: 2.32, sys: 0.08, mem: 470384 ko)
solvable/nilpotent.vo (real: 2.40, user: 2.32, sys: 0.08, mem: 555472 ko)
ssreflect/choice.vo (real: 2.04, user: 1.98, sys: 0.05, mem: 471896 ko)
ssreflect/path.vo (real: 1.92, user: 1.85, sys: 0.06, mem: 457084 ko)
fingroup/perm.vo (real: 1.88, user: 1.81, sys: 0.07, mem: 482784 ko)
fingroup/automorphism.vo (real: 1.88, user: 1.80, sys: 0.07, mem: 470384 ko)
algebra/all_algebra.vo (real: 1.80, user: 1.65, sys: 0.14, mem: 684564 ko)
solvable/gfunctor.vo (real: 1.67, user: 1.59, sys: 0.08, mem: 479708 ko)
solvable/primitive_action.vo (real: 1.52, user: 1.39, sys: 0.12, mem: 554704 ko)
ssreflect/fingraph.vo (real: 1.48, user: 1.43, sys: 0.04, mem: 458856 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.40, sys: 0.04, mem: 466804 ko)
ssreflect/binomial.vo (real: 1.42, user: 1.36, sys: 0.05, mem: 469160 ko)
character/all_character.vo (real: 1.36, user: 1.30, sys: 0.06, mem: 722772 ko)
ssreflect/all_ssreflect.vo (real: 1.33, user: 1.26, sys: 0.07, mem: 522160 ko)
ssreflect/generic_quotient.vo (real: 1.30, user: 1.28, sys: 0.02, mem: 478332 ko)
field/all_field.vo (real: 1.26, user: 1.18, sys: 0.07, mem: 704796 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.11, sys: 0.03, mem: 473008 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.02, sys: 0.08, mem: 462764 ko)
ssreflect/eqtype.vo (real: 1.07, user: 0.99, sys: 0.08, mem: 449752 ko)
solvable/commutator.vo (real: 1.06, user: 0.99, sys: 0.06, mem: 482500 ko)
ssreflect/div.vo (real: 1.03, user: 0.98, sys: 0.05, mem: 446892 ko)
solvable/all_solvable.vo (real: 0.95, user: 0.88, sys: 0.07, mem: 606176 ko)
fingroup/presentation.vo (real: 0.53, user: 0.45, sys: 0.08, mem: 468468 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.36, sys: 0.03, mem: 449496 ko)
fingroup/all_fingroup.vo (real: 0.36, user: 0.30, sys: 0.06, mem: 465136 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.01, mem: 141620 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 112360 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 86488 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.01, sys: 0.03, mem: 75328 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.01, sys: 0.02, mem: 72096 ko)

Add a proper type for order displays: 15:00.66 (1469436ko)

891.25user 9.39system 15:00.66elapsed 99%CPU (0avgtext+0avgdata 1469436maxresident)k
ssreflect/order.vo (real: 109.21, user: 108.96, sys: 0.22, mem: 1469436 ko)
algebra/ssrnum.vo (real: 59.42, user: 59.25, sys: 0.17, mem: 1184584 ko)
algebra/ssralg.vo (real: 59.09, user: 58.86, sys: 0.22, mem: 1353856 ko)
algebra/matrix.vo (real: 36.83, user: 36.64, sys: 0.19, mem: 1226772 ko)
algebra/finalg.vo (real: 30.90, user: 30.78, sys: 0.12, mem: 900944 ko)
character/mxrepresentation.vo (real: 28.09, user: 27.91, sys: 0.17, mem: 1008680 ko)
field/algebraics_fundamentals.vo (real: 26.51, user: 26.32, sys: 0.19, mem: 1352276 ko)
solvable/extremal.vo (real: 26.11, user: 26.00, sys: 0.11, mem: 860108 ko)
field/galois.vo (real: 22.30, user: 22.18, sys: 0.12, mem: 907536 ko)
field/finfield.vo (real: 20.41, user: 20.26, sys: 0.15, mem: 1068644 ko)
character/character.vo (real: 20.10, user: 19.88, sys: 0.21, mem: 970976 ko)
character/classfun.vo (real: 19.89, user: 19.69, sys: 0.20, mem: 1078356 ko)
field/algC.vo (real: 19.25, user: 19.05, sys: 0.20, mem: 1072448 ko)
solvable/extraspecial.vo (real: 17.56, user: 17.44, sys: 0.12, mem: 784496 ko)
field/fieldext.vo (real: 17.29, user: 17.06, sys: 0.22, mem: 1010160 ko)
algebra/mxpoly.vo (real: 14.05, user: 13.90, sys: 0.15, mem: 771348 ko)
character/inertia.vo (real: 12.52, user: 12.41, sys: 0.11, mem: 864788 ko)
algebra/interval.vo (real: 12.13, user: 11.97, sys: 0.16, mem: 895252 ko)
field/closed_field.vo (real: 11.73, user: 11.59, sys: 0.13, mem: 888212 ko)
solvable/burnside_app.vo (real: 11.70, user: 11.62, sys: 0.08, mem: 654636 ko)
algebra/poly.vo (real: 11.57, user: 11.42, sys: 0.12, mem: 761732 ko)
algebra/mxalgebra.vo (real: 11.31, user: 11.23, sys: 0.08, mem: 768680 ko)
field/algnum.vo (real: 10.86, user: 10.69, sys: 0.17, mem: 842324 ko)
algebra/polydiv.vo (real: 10.53, user: 10.37, sys: 0.16, mem: 607736 ko)
algebra/vector.vo (real: 10.16, user: 10.02, sys: 0.13, mem: 796092 ko)
field/falgebra.vo (real: 9.95, user: 9.91, sys: 0.04, mem: 792080 ko)
algebra/countalg.vo (real: 9.94, user: 9.84, sys: 0.09, mem: 660316 ko)
character/vcharacter.vo (real: 9.91, user: 9.82, sys: 0.09, mem: 832284 ko)
field/qfpoly.vo (real: 9.85, user: 9.75, sys: 0.10, mem: 805464 ko)
character/integral_char.vo (real: 9.54, user: 9.43, sys: 0.10, mem: 839504 ko)
solvable/hall.vo (real: 9.50, user: 9.41, sys: 0.08, mem: 609552 ko)
solvable/maximal.vo (real: 9.16, user: 9.09, sys: 0.06, mem: 624836 ko)
algebra/rat.vo (real: 8.93, user: 8.82, sys: 0.11, mem: 780564 ko)
field/separable.vo (real: 8.54, user: 8.42, sys: 0.11, mem: 702940 ko)
fingroup/gproduct.vo (real: 8.52, user: 8.38, sys: 0.14, mem: 562196 ko)
algebra/qpoly.vo (real: 8.44, user: 8.33, sys: 0.10, mem: 761456 ko)
algebra/ssrint.vo (real: 8.29, user: 8.23, sys: 0.06, mem: 767764 ko)
character/mxabelem.vo (real: 8.04, user: 7.95, sys: 0.09, mem: 694728 ko)
solvable/abelian.vo (real: 7.72, user: 7.60, sys: 0.12, mem: 619604 ko)
algebra/ring_quotient.vo (real: 7.40, user: 7.34, sys: 0.06, mem: 638992 ko)
algebra/intdiv.vo (real: 6.54, user: 6.40, sys: 0.13, mem: 738712 ko)
fingroup/action.vo (real: 6.25, user: 6.16, sys: 0.08, mem: 538968 ko)
fingroup/fingroup.vo (real: 5.14, user: 5.09, sys: 0.05, mem: 547964 ko)
algebra/zmodp.vo (real: 5.00, user: 4.87, sys: 0.12, mem: 589568 ko)
solvable/finmodule.vo (real: 4.87, user: 4.80, sys: 0.07, mem: 594688 ko)
solvable/alt.vo (real: 4.80, user: 4.73, sys: 0.07, mem: 569828 ko)
solvable/center.vo (real: 4.64, user: 4.53, sys: 0.09, mem: 567324 ko)
algebra/polyXY.vo (real: 4.61, user: 4.45, sys: 0.15, mem: 638392 ko)
ssreflect/seq.vo (real: 4.15, user: 4.11, sys: 0.03, mem: 525784 ko)
ssreflect/bigop.vo (real: 4.14, user: 4.05, sys: 0.08, mem: 539092 ko)
fingroup/morphism.vo (real: 4.12, user: 4.08, sys: 0.03, mem: 491568 ko)
ssreflect/finset.vo (real: 3.91, user: 3.88, sys: 0.03, mem: 514688 ko)
algebra/archimedean.vo (real: 3.85, user: 3.79, sys: 0.06, mem: 658944 ko)
solvable/pgroup.vo (real: 3.80, user: 3.72, sys: 0.08, mem: 569588 ko)
solvable/frobenius.vo (real: 3.80, user: 3.75, sys: 0.04, mem: 570460 ko)
solvable/jordanholder.vo (real: 3.69, user: 3.64, sys: 0.05, mem: 557360 ko)
solvable/cyclic.vo (real: 3.66, user: 3.61, sys: 0.05, mem: 568524 ko)
field/cyclotomic.vo (real: 3.53, user: 3.44, sys: 0.09, mem: 716900 ko)
ssreflect/fintype.vo (real: 3.33, user: 3.20, sys: 0.13, mem: 518600 ko)
algebra/fraction.vo (real: 3.31, user: 3.21, sys: 0.10, mem: 560484 ko)
all/all.vo (real: 3.29, user: 3.20, sys: 0.08, mem: 780956 ko)
fingroup/quotient.vo (real: 3.17, user: 3.12, sys: 0.05, mem: 486432 ko)
solvable/gseries.vo (real: 2.98, user: 2.85, sys: 0.13, mem: 553872 ko)
solvable/sylow.vo (real: 2.91, user: 2.82, sys: 0.08, mem: 562536 ko)
solvable/nilpotent.vo (real: 2.61, user: 2.56, sys: 0.05, mem: 555756 ko)
ssreflect/prime.vo (real: 2.41, user: 2.31, sys: 0.09, mem: 470768 ko)
ssreflect/choice.vo (real: 2.04, user: 1.99, sys: 0.04, mem: 471608 ko)
fingroup/automorphism.vo (real: 2.00, user: 1.88, sys: 0.12, mem: 471236 ko)
fingroup/perm.vo (real: 1.97, user: 1.87, sys: 0.10, mem: 482640 ko)
algebra/all_algebra.vo (real: 1.92, user: 1.87, sys: 0.05, mem: 686720 ko)
ssreflect/fingraph.vo (real: 1.90, user: 1.76, sys: 0.14, mem: 454000 ko)
ssreflect/path.vo (real: 1.89, user: 1.85, sys: 0.04, mem: 456840 ko)
solvable/primitive_action.vo (real: 1.88, user: 1.83, sys: 0.05, mem: 554324 ko)
solvable/gfunctor.vo (real: 1.80, user: 1.73, sys: 0.07, mem: 478520 ko)
character/all_character.vo (real: 1.45, user: 1.35, sys: 0.10, mem: 722500 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.38, sys: 0.06, mem: 461628 ko)
ssreflect/binomial.vo (real: 1.43, user: 1.38, sys: 0.05, mem: 468176 ko)
ssreflect/generic_quotient.vo (real: 1.42, user: 1.37, sys: 0.05, mem: 476996 ko)
ssreflect/all_ssreflect.vo (real: 1.36, user: 1.30, sys: 0.06, mem: 522248 ko)
field/all_field.vo (real: 1.34, user: 1.27, sys: 0.07, mem: 703924 ko)
solvable/commutator.vo (real: 1.16, user: 1.10, sys: 0.05, mem: 479268 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.07, sys: 0.07, mem: 473104 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.08, sys: 0.01, mem: 463664 ko)
ssreflect/eqtype.vo (real: 1.07, user: 1.00, sys: 0.06, mem: 450412 ko)
ssreflect/div.vo (real: 1.02, user: 0.93, sys: 0.08, mem: 446272 ko)
solvable/all_solvable.vo (real: 0.94, user: 0.85, sys: 0.09, mem: 606096 ko)
fingroup/presentation.vo (real: 0.56, user: 0.50, sys: 0.06, mem: 467748 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.31, sys: 0.09, mem: 451948 ko)
fingroup/all_fingroup.vo (real: 0.32, user: 0.25, sys: 0.07, mem: 465228 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 141456 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.02, sys: 0.04, mem: 113296 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.01, sys: 0.04, mem: 86104 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.03, sys: 0.01, mem: 74980 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 73268 ko)

Make dual_display involutive: 14:51.45 (1468148ko)

882.61user 8.71system 14:51.45elapsed 99%CPU (0avgtext+0avgdata 1468148maxresident)k
ssreflect/order.vo (real: 109.14, user: 108.86, sys: 0.26, mem: 1468148 ko)
algebra/ssrnum.vo (real: 59.37, user: 59.18, sys: 0.18, mem: 1182476 ko)
algebra/ssralg.vo (real: 59.17, user: 58.92, sys: 0.25, mem: 1353232 ko)
algebra/matrix.vo (real: 36.35, user: 36.16, sys: 0.19, mem: 1241580 ko)
character/mxrepresentation.vo (real: 27.93, user: 27.75, sys: 0.18, mem: 1007308 ko)
algebra/finalg.vo (real: 26.94, user: 26.85, sys: 0.08, mem: 902020 ko)
field/algebraics_fundamentals.vo (real: 26.14, user: 25.99, sys: 0.14, mem: 1350512 ko)
solvable/extremal.vo (real: 25.70, user: 25.60, sys: 0.10, mem: 860424 ko)
field/galois.vo (real: 22.35, user: 22.19, sys: 0.15, mem: 904368 ko)
field/finfield.vo (real: 21.07, user: 20.85, sys: 0.22, mem: 1073472 ko)
character/character.vo (real: 20.03, user: 19.92, sys: 0.11, mem: 966784 ko)
character/classfun.vo (real: 19.72, user: 19.50, sys: 0.22, mem: 1073168 ko)
field/algC.vo (real: 18.60, user: 18.49, sys: 0.11, mem: 1076804 ko)
solvable/extraspecial.vo (real: 17.48, user: 17.37, sys: 0.09, mem: 784648 ko)
field/fieldext.vo (real: 17.42, user: 17.30, sys: 0.12, mem: 1011908 ko)
algebra/mxpoly.vo (real: 13.99, user: 13.91, sys: 0.06, mem: 769896 ko)
character/inertia.vo (real: 12.86, user: 12.73, sys: 0.13, mem: 861356 ko)
field/closed_field.vo (real: 12.05, user: 11.94, sys: 0.11, mem: 887152 ko)
solvable/burnside_app.vo (real: 11.74, user: 11.67, sys: 0.06, mem: 655472 ko)
algebra/poly.vo (real: 11.58, user: 11.45, sys: 0.11, mem: 761780 ko)
algebra/interval.vo (real: 11.43, user: 11.30, sys: 0.11, mem: 893796 ko)
algebra/mxalgebra.vo (real: 11.20, user: 11.10, sys: 0.10, mem: 770572 ko)
field/algnum.vo (real: 10.65, user: 10.55, sys: 0.09, mem: 842508 ko)
algebra/vector.vo (real: 10.17, user: 10.05, sys: 0.12, mem: 795992 ko)
algebra/countalg.vo (real: 10.05, user: 9.95, sys: 0.09, mem: 660576 ko)
character/integral_char.vo (real: 9.80, user: 9.68, sys: 0.11, mem: 844976 ko)
field/falgebra.vo (real: 9.71, user: 9.58, sys: 0.13, mem: 796800 ko)
character/vcharacter.vo (real: 9.65, user: 9.54, sys: 0.11, mem: 827700 ko)
field/qfpoly.vo (real: 9.62, user: 9.53, sys: 0.08, mem: 807668 ko)
solvable/hall.vo (real: 9.16, user: 9.09, sys: 0.05, mem: 609712 ko)
algebra/qpoly.vo (real: 8.84, user: 8.71, sys: 0.13, mem: 761476 ko)
algebra/rat.vo (real: 8.80, user: 8.71, sys: 0.09, mem: 778768 ko)
solvable/maximal.vo (real: 8.78, user: 8.70, sys: 0.07, mem: 624300 ko)
algebra/polydiv.vo (real: 8.69, user: 8.61, sys: 0.08, mem: 602804 ko)
field/separable.vo (real: 8.64, user: 8.53, sys: 0.11, mem: 702724 ko)
algebra/ssrint.vo (real: 8.60, user: 8.48, sys: 0.12, mem: 767068 ko)
fingroup/gproduct.vo (real: 8.37, user: 8.29, sys: 0.08, mem: 564256 ko)
character/mxabelem.vo (real: 8.11, user: 8.01, sys: 0.08, mem: 692620 ko)
solvable/abelian.vo (real: 7.78, user: 7.70, sys: 0.08, mem: 619176 ko)
algebra/ring_quotient.vo (real: 7.30, user: 7.24, sys: 0.04, mem: 638932 ko)
fingroup/action.vo (real: 6.34, user: 6.24, sys: 0.10, mem: 538644 ko)
algebra/intdiv.vo (real: 6.34, user: 6.21, sys: 0.13, mem: 739108 ko)
solvable/alt.vo (real: 5.13, user: 4.94, sys: 0.19, mem: 569064 ko)
fingroup/fingroup.vo (real: 5.08, user: 4.98, sys: 0.09, mem: 550348 ko)
solvable/finmodule.vo (real: 4.91, user: 4.88, sys: 0.03, mem: 590028 ko)
solvable/center.vo (real: 4.72, user: 4.67, sys: 0.04, mem: 566216 ko)
fingroup/morphism.vo (real: 4.39, user: 4.36, sys: 0.02, mem: 491572 ko)
ssreflect/seq.vo (real: 4.22, user: 4.19, sys: 0.03, mem: 524816 ko)
solvable/pgroup.vo (real: 4.21, user: 4.12, sys: 0.08, mem: 570668 ko)
ssreflect/bigop.vo (real: 4.15, user: 4.06, sys: 0.09, mem: 538056 ko)
algebra/polyXY.vo (real: 4.10, user: 4.05, sys: 0.05, mem: 638628 ko)
algebra/archimedean.vo (real: 3.97, user: 3.92, sys: 0.05, mem: 661800 ko)
ssreflect/finset.vo (real: 3.90, user: 3.84, sys: 0.06, mem: 514668 ko)
algebra/zmodp.vo (real: 3.79, user: 3.72, sys: 0.07, mem: 587580 ko)
algebra/fraction.vo (real: 3.73, user: 3.66, sys: 0.07, mem: 560748 ko)
solvable/frobenius.vo (real: 3.69, user: 3.61, sys: 0.08, mem: 572676 ko)
solvable/cyclic.vo (real: 3.69, user: 3.63, sys: 0.06, mem: 569108 ko)
solvable/jordanholder.vo (real: 3.68, user: 3.60, sys: 0.08, mem: 557184 ko)
field/cyclotomic.vo (real: 3.38, user: 3.28, sys: 0.09, mem: 716248 ko)
ssreflect/fintype.vo (real: 3.34, user: 3.27, sys: 0.07, mem: 518776 ko)
fingroup/quotient.vo (real: 3.33, user: 3.27, sys: 0.06, mem: 485128 ko)
all/all.vo (real: 3.24, user: 3.12, sys: 0.12, mem: 778388 ko)
solvable/gseries.vo (real: 2.99, user: 2.93, sys: 0.06, mem: 553324 ko)
solvable/sylow.vo (real: 2.87, user: 2.75, sys: 0.12, mem: 559256 ko)
solvable/nilpotent.vo (real: 2.54, user: 2.48, sys: 0.06, mem: 557636 ko)
ssreflect/prime.vo (real: 2.40, user: 2.34, sys: 0.05, mem: 470676 ko)
ssreflect/choice.vo (real: 2.03, user: 1.95, sys: 0.07, mem: 474336 ko)
fingroup/perm.vo (real: 1.98, user: 1.96, sys: 0.02, mem: 483000 ko)
fingroup/automorphism.vo (real: 1.93, user: 1.86, sys: 0.06, mem: 470912 ko)
algebra/all_algebra.vo (real: 1.92, user: 1.83, sys: 0.09, mem: 684704 ko)
ssreflect/path.vo (real: 1.90, user: 1.84, sys: 0.06, mem: 456952 ko)
solvable/primitive_action.vo (real: 1.81, user: 1.72, sys: 0.09, mem: 554604 ko)
solvable/gfunctor.vo (real: 1.78, user: 1.72, sys: 0.06, mem: 479548 ko)
ssreflect/fingraph.vo (real: 1.46, user: 1.34, sys: 0.11, mem: 455316 ko)
character/all_character.vo (real: 1.46, user: 1.38, sys: 0.07, mem: 720824 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.40, sys: 0.04, mem: 461816 ko)
ssreflect/binomial.vo (real: 1.42, user: 1.36, sys: 0.06, mem: 469220 ko)
field/all_field.vo (real: 1.41, user: 1.28, sys: 0.13, mem: 704820 ko)
ssreflect/generic_quotient.vo (real: 1.39, user: 1.34, sys: 0.04, mem: 475864 ko)
ssreflect/all_ssreflect.vo (real: 1.27, user: 1.21, sys: 0.05, mem: 524304 ko)
ssreflect/tuple.vo (real: 1.17, user: 1.11, sys: 0.05, mem: 476108 ko)
solvable/commutator.vo (real: 1.15, user: 1.07, sys: 0.07, mem: 479056 ko)
ssreflect/finfun.vo (real: 1.12, user: 1.08, sys: 0.03, mem: 462668 ko)
ssreflect/eqtype.vo (real: 1.06, user: 0.97, sys: 0.09, mem: 449996 ko)
ssreflect/div.vo (real: 1.03, user: 0.96, sys: 0.07, mem: 451516 ko)
solvable/all_solvable.vo (real: 0.96, user: 0.86, sys: 0.10, mem: 606484 ko)
fingroup/presentation.vo (real: 0.55, user: 0.47, sys: 0.08, mem: 468992 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.37, sys: 0.03, mem: 449576 ko)
fingroup/all_fingroup.vo (real: 0.35, user: 0.27, sys: 0.07, mem: 466396 ko)
ssreflect/ssrbool.vo (real: 0.09, user: 0.08, sys: 0.00, mem: 141152 ko)
ssreflect/ssrfun.vo (real: 0.08, user: 0.07, sys: 0.01, mem: 111896 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 85808 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 75976 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.03, sys: 0.01, mem: 73480 ko)

Make dual involutive: 14:44.62 (1465372ko)

875.06user 9.35system 14:44.62elapsed 99%CPU (0avgtext+0avgdata 1465372maxresident)k
ssreflect/order.vo (real: 109.23, user: 108.96, sys: 0.27, mem: 1465372 ko)
algebra/ssralg.vo (real: 59.20, user: 59.02, sys: 0.16, mem: 1353012 ko)
algebra/ssrnum.vo (real: 59.16, user: 58.97, sys: 0.19, mem: 1207092 ko)
algebra/matrix.vo (real: 34.99, user: 34.82, sys: 0.17, mem: 1245480 ko)
character/mxrepresentation.vo (real: 28.35, user: 28.16, sys: 0.16, mem: 1012796 ko)
field/algebraics_fundamentals.vo (real: 26.45, user: 26.20, sys: 0.23, mem: 1355316 ko)
algebra/finalg.vo (real: 25.97, user: 25.88, sys: 0.09, mem: 900980 ko)
solvable/extremal.vo (real: 25.66, user: 25.51, sys: 0.13, mem: 870776 ko)
field/galois.vo (real: 22.32, user: 22.21, sys: 0.11, mem: 902796 ko)
field/finfield.vo (real: 20.46, user: 20.34, sys: 0.12, mem: 1059020 ko)
character/classfun.vo (real: 19.89, user: 19.69, sys: 0.19, mem: 1079072 ko)
character/character.vo (real: 19.29, user: 19.13, sys: 0.14, mem: 966260 ko)
field/algC.vo (real: 18.13, user: 17.93, sys: 0.19, mem: 1085428 ko)
solvable/extraspecial.vo (real: 17.51, user: 17.40, sys: 0.11, mem: 784748 ko)
field/fieldext.vo (real: 17.45, user: 17.33, sys: 0.11, mem: 979556 ko)
algebra/mxpoly.vo (real: 13.36, user: 13.24, sys: 0.10, mem: 769608 ko)
character/inertia.vo (real: 12.88, user: 12.76, sys: 0.12, mem: 856036 ko)
field/closed_field.vo (real: 11.80, user: 11.68, sys: 0.11, mem: 866496 ko)
algebra/poly.vo (real: 11.71, user: 11.56, sys: 0.14, mem: 761404 ko)
solvable/burnside_app.vo (real: 11.66, user: 11.55, sys: 0.11, mem: 655636 ko)
algebra/interval.vo (real: 11.59, user: 11.50, sys: 0.09, mem: 884832 ko)
field/algnum.vo (real: 10.70, user: 10.57, sys: 0.13, mem: 841452 ko)
algebra/mxalgebra.vo (real: 10.55, user: 10.40, sys: 0.14, mem: 768768 ko)
character/integral_char.vo (real: 10.03, user: 9.91, sys: 0.10, mem: 831404 ko)
algebra/vector.vo (real: 10.03, user: 9.95, sys: 0.08, mem: 783592 ko)
algebra/countalg.vo (real: 9.96, user: 9.83, sys: 0.12, mem: 663212 ko)
field/falgebra.vo (real: 9.71, user: 9.54, sys: 0.16, mem: 806988 ko)
character/vcharacter.vo (real: 9.67, user: 9.53, sys: 0.13, mem: 818624 ko)
field/qfpoly.vo (real: 9.24, user: 9.18, sys: 0.05, mem: 813892 ko)
solvable/hall.vo (real: 9.16, user: 9.08, sys: 0.07, mem: 609640 ko)
algebra/rat.vo (real: 8.99, user: 8.88, sys: 0.11, mem: 768964 ko)
fingroup/gproduct.vo (real: 8.85, user: 8.77, sys: 0.08, mem: 562248 ko)
solvable/maximal.vo (real: 8.80, user: 8.71, sys: 0.08, mem: 624284 ko)
field/separable.vo (real: 8.66, user: 8.57, sys: 0.08, mem: 707276 ko)
algebra/qpoly.vo (real: 8.44, user: 8.37, sys: 0.07, mem: 769608 ko)
algebra/ssrint.vo (real: 8.32, user: 8.20, sys: 0.12, mem: 762784 ko)
algebra/polydiv.vo (real: 8.27, user: 8.09, sys: 0.15, mem: 603384 ko)
solvable/abelian.vo (real: 8.20, user: 8.06, sys: 0.12, mem: 621592 ko)
character/mxabelem.vo (real: 8.13, user: 8.00, sys: 0.12, mem: 694836 ko)
algebra/ring_quotient.vo (real: 7.76, user: 7.66, sys: 0.07, mem: 643324 ko)
algebra/intdiv.vo (real: 6.62, user: 6.55, sys: 0.06, mem: 735884 ko)
fingroup/action.vo (real: 6.23, user: 6.13, sys: 0.10, mem: 537980 ko)
fingroup/fingroup.vo (real: 5.05, user: 4.96, sys: 0.08, mem: 547292 ko)
solvable/finmodule.vo (real: 4.89, user: 4.81, sys: 0.08, mem: 589896 ko)
solvable/center.vo (real: 4.74, user: 4.65, sys: 0.08, mem: 565848 ko)
solvable/alt.vo (real: 4.66, user: 4.59, sys: 0.06, mem: 571808 ko)
ssreflect/seq.vo (real: 4.16, user: 4.09, sys: 0.07, mem: 524944 ko)
ssreflect/bigop.vo (real: 4.15, user: 4.04, sys: 0.11, mem: 541764 ko)
fingroup/morphism.vo (real: 4.04, user: 3.95, sys: 0.07, mem: 491772 ko)
ssreflect/finset.vo (real: 3.89, user: 3.81, sys: 0.08, mem: 515752 ko)
solvable/cyclic.vo (real: 3.83, user: 3.74, sys: 0.09, mem: 568524 ko)
solvable/pgroup.vo (real: 3.82, user: 3.71, sys: 0.11, mem: 572436 ko)
algebra/archimedean.vo (real: 3.81, user: 3.72, sys: 0.07, mem: 658424 ko)
algebra/polyXY.vo (real: 3.80, user: 3.69, sys: 0.11, mem: 644672 ko)
all/all.vo (real: 3.70, user: 3.56, sys: 0.13, mem: 781084 ko)
solvable/jordanholder.vo (real: 3.63, user: 3.56, sys: 0.07, mem: 557300 ko)
solvable/frobenius.vo (real: 3.62, user: 3.50, sys: 0.11, mem: 572476 ko)
algebra/zmodp.vo (real: 3.62, user: 3.53, sys: 0.08, mem: 589028 ko)
field/cyclotomic.vo (real: 3.40, user: 3.33, sys: 0.07, mem: 717120 ko)
algebra/fraction.vo (real: 3.40, user: 3.31, sys: 0.09, mem: 561596 ko)
ssreflect/fintype.vo (real: 3.32, user: 3.25, sys: 0.07, mem: 521324 ko)
fingroup/quotient.vo (real: 3.15, user: 3.05, sys: 0.09, mem: 485964 ko)
solvable/gseries.vo (real: 2.97, user: 2.87, sys: 0.09, mem: 553588 ko)
solvable/sylow.vo (real: 2.73, user: 2.64, sys: 0.09, mem: 557744 ko)
solvable/nilpotent.vo (real: 2.55, user: 2.49, sys: 0.05, mem: 555976 ko)
ssreflect/prime.vo (real: 2.41, user: 2.34, sys: 0.07, mem: 470536 ko)
ssreflect/choice.vo (real: 2.03, user: 1.95, sys: 0.07, mem: 472824 ko)
fingroup/perm.vo (real: 1.97, user: 1.85, sys: 0.11, mem: 482796 ko)
algebra/all_algebra.vo (real: 1.94, user: 1.82, sys: 0.11, mem: 687196 ko)
ssreflect/path.vo (real: 1.88, user: 1.83, sys: 0.05, mem: 456036 ko)
fingroup/automorphism.vo (real: 1.87, user: 1.83, sys: 0.04, mem: 473988 ko)
solvable/gfunctor.vo (real: 1.78, user: 1.72, sys: 0.05, mem: 479852 ko)
solvable/primitive_action.vo (real: 1.59, user: 1.53, sys: 0.06, mem: 553424 ko)
ssreflect/fingraph.vo (real: 1.51, user: 1.43, sys: 0.07, mem: 455492 ko)
ssreflect/binomial.vo (real: 1.46, user: 1.42, sys: 0.03, mem: 467704 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.36, sys: 0.07, mem: 461336 ko)
ssreflect/generic_quotient.vo (real: 1.42, user: 1.37, sys: 0.04, mem: 475388 ko)
character/all_character.vo (real: 1.42, user: 1.33, sys: 0.09, mem: 723044 ko)
field/all_field.vo (real: 1.31, user: 1.21, sys: 0.10, mem: 704040 ko)
ssreflect/all_ssreflect.vo (real: 1.28, user: 1.20, sys: 0.07, mem: 523924 ko)
solvable/commutator.vo (real: 1.17, user: 1.10, sys: 0.04, mem: 480008 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.09, sys: 0.05, mem: 473400 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.07, sys: 0.03, mem: 465948 ko)
ssreflect/eqtype.vo (real: 1.06, user: 0.94, sys: 0.12, mem: 451408 ko)
ssreflect/div.vo (real: 1.02, user: 0.96, sys: 0.06, mem: 446508 ko)
solvable/all_solvable.vo (real: 0.93, user: 0.85, sys: 0.08, mem: 608012 ko)
fingroup/presentation.vo (real: 0.56, user: 0.48, sys: 0.06, mem: 467420 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.33, sys: 0.07, mem: 449924 ko)
fingroup/all_fingroup.vo (real: 0.32, user: 0.24, sys: 0.07, mem: 465296 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 143312 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 113292 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.05, sys: 0.00, mem: 85576 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.03, sys: 0.01, mem: 75144 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 73012 ko)

Add semilattice structures: 16:17.89 (1513924ko)

968.71user 9.13system 16:17.89elapsed 99%CPU (0avgtext+0avgdata 1513924maxresident)k
ssreflect/order.vo (real: 165.27, user: 164.96, sys: 0.31, mem: 1513924 ko)
algebra/ssrnum.vo (real: 68.74, user: 68.61, sys: 0.11, mem: 1231672 ko)
algebra/ssralg.vo (real: 59.18, user: 58.96, sys: 0.22, mem: 1351864 ko)
algebra/matrix.vo (real: 39.73, user: 39.54, sys: 0.18, mem: 1342824 ko)
character/mxrepresentation.vo (real: 28.97, user: 28.79, sys: 0.18, mem: 1031156 ko)
field/algebraics_fundamentals.vo (real: 26.75, user: 26.53, sys: 0.21, mem: 1403604 ko)
solvable/extremal.vo (real: 25.83, user: 25.71, sys: 0.12, mem: 864832 ko)
algebra/finalg.vo (real: 25.78, user: 25.66, sys: 0.11, mem: 901424 ko)
field/galois.vo (real: 22.73, user: 22.58, sys: 0.15, mem: 938060 ko)
field/finfield.vo (real: 21.12, user: 20.86, sys: 0.24, mem: 1081472 ko)
character/classfun.vo (real: 21.09, user: 20.96, sys: 0.13, mem: 1137176 ko)
field/algC.vo (real: 20.30, user: 20.10, sys: 0.20, mem: 1157764 ko)
character/character.vo (real: 19.93, user: 19.72, sys: 0.20, mem: 1008092 ko)
field/fieldext.vo (real: 17.83, user: 17.69, sys: 0.13, mem: 1014376 ko)
solvable/extraspecial.vo (real: 17.65, user: 17.56, sys: 0.07, mem: 790716 ko)
algebra/mxpoly.vo (real: 14.33, user: 14.25, sys: 0.08, mem: 781844 ko)
algebra/interval.vo (real: 14.03, user: 13.91, sys: 0.11, mem: 986612 ko)
character/inertia.vo (real: 13.21, user: 13.09, sys: 0.11, mem: 881492 ko)
field/closed_field.vo (real: 12.21, user: 12.11, sys: 0.10, mem: 897720 ko)
solvable/burnside_app.vo (real: 11.85, user: 11.76, sys: 0.09, mem: 657572 ko)
algebra/mxalgebra.vo (real: 11.85, user: 11.74, sys: 0.11, mem: 802544 ko)
algebra/poly.vo (real: 11.54, user: 11.39, sys: 0.14, mem: 762260 ko)
field/algnum.vo (real: 10.86, user: 10.76, sys: 0.10, mem: 872064 ko)
algebra/vector.vo (real: 10.49, user: 10.39, sys: 0.10, mem: 819432 ko)
character/vcharacter.vo (real: 10.29, user: 10.19, sys: 0.10, mem: 857376 ko)
character/integral_char.vo (real: 10.23, user: 10.18, sys: 0.05, mem: 867228 ko)
algebra/rat.vo (real: 10.21, user: 10.13, sys: 0.08, mem: 834368 ko)
field/falgebra.vo (real: 10.05, user: 9.90, sys: 0.14, mem: 806412 ko)
algebra/countalg.vo (real: 9.95, user: 9.89, sys: 0.06, mem: 661152 ko)
algebra/ssrint.vo (real: 9.94, user: 9.86, sys: 0.08, mem: 827380 ko)
solvable/hall.vo (real: 9.48, user: 9.38, sys: 0.09, mem: 609608 ko)
field/qfpoly.vo (real: 9.43, user: 9.31, sys: 0.11, mem: 832560 ko)
solvable/maximal.vo (real: 8.82, user: 8.75, sys: 0.06, mem: 623968 ko)
algebra/qpoly.vo (real: 8.76, user: 8.65, sys: 0.11, mem: 777712 ko)
field/separable.vo (real: 8.75, user: 8.63, sys: 0.12, mem: 713000 ko)
character/mxabelem.vo (real: 8.41, user: 8.33, sys: 0.07, mem: 705204 ko)
algebra/polydiv.vo (real: 8.22, user: 8.15, sys: 0.05, mem: 604448 ko)
solvable/abelian.vo (real: 8.19, user: 8.12, sys: 0.07, mem: 621728 ko)
fingroup/gproduct.vo (real: 8.12, user: 8.05, sys: 0.06, mem: 563952 ko)
algebra/ring_quotient.vo (real: 7.36, user: 7.21, sys: 0.14, mem: 639704 ko)
algebra/intdiv.vo (real: 6.92, user: 6.84, sys: 0.08, mem: 764092 ko)
fingroup/action.vo (real: 6.06, user: 6.02, sys: 0.03, mem: 537840 ko)
fingroup/fingroup.vo (real: 5.23, user: 5.16, sys: 0.07, mem: 548132 ko)
solvable/finmodule.vo (real: 4.84, user: 4.76, sys: 0.08, mem: 591128 ko)
solvable/center.vo (real: 4.73, user: 4.64, sys: 0.09, mem: 570088 ko)
solvable/alt.vo (real: 4.71, user: 4.63, sys: 0.07, mem: 569916 ko)
algebra/archimedean.vo (real: 4.37, user: 4.28, sys: 0.08, mem: 690648 ko)
solvable/pgroup.vo (real: 4.26, user: 4.15, sys: 0.11, mem: 569712 ko)
all/all.vo (real: 4.24, user: 4.08, sys: 0.14, mem: 799144 ko)
ssreflect/seq.vo (real: 4.17, user: 4.08, sys: 0.09, mem: 524876 ko)
ssreflect/bigop.vo (real: 4.14, user: 4.05, sys: 0.09, mem: 539764 ko)
algebra/polyXY.vo (real: 4.09, user: 4.02, sys: 0.07, mem: 650804 ko)
fingroup/morphism.vo (real: 3.99, user: 3.92, sys: 0.06, mem: 491468 ko)
ssreflect/finset.vo (real: 3.89, user: 3.82, sys: 0.07, mem: 517840 ko)
solvable/frobenius.vo (real: 3.72, user: 3.61, sys: 0.10, mem: 569404 ko)
solvable/cyclic.vo (real: 3.72, user: 3.65, sys: 0.07, mem: 567584 ko)
solvable/jordanholder.vo (real: 3.64, user: 3.57, sys: 0.07, mem: 559212 ko)
algebra/zmodp.vo (real: 3.61, user: 3.50, sys: 0.10, mem: 586632 ko)
field/cyclotomic.vo (real: 3.53, user: 3.48, sys: 0.05, mem: 729336 ko)
algebra/fraction.vo (real: 3.40, user: 3.34, sys: 0.06, mem: 561808 ko)
ssreflect/fintype.vo (real: 3.32, user: 3.21, sys: 0.09, mem: 519272 ko)
fingroup/quotient.vo (real: 3.16, user: 3.08, sys: 0.08, mem: 485896 ko)
algebra/all_algebra.vo (real: 3.09, user: 2.97, sys: 0.11, mem: 698516 ko)
solvable/gseries.vo (real: 3.04, user: 2.97, sys: 0.07, mem: 552388 ko)
solvable/sylow.vo (real: 3.02, user: 2.95, sys: 0.06, mem: 558248 ko)
ssreflect/all_ssreflect.vo (real: 2.62, user: 2.50, sys: 0.12, mem: 535732 ko)
solvable/nilpotent.vo (real: 2.53, user: 2.46, sys: 0.07, mem: 556076 ko)
ssreflect/prime.vo (real: 2.39, user: 2.31, sys: 0.08, mem: 470484 ko)
ssreflect/choice.vo (real: 2.04, user: 1.97, sys: 0.05, mem: 473076 ko)
ssreflect/fingraph.vo (real: 1.97, user: 1.87, sys: 0.09, mem: 453896 ko)
ssreflect/path.vo (real: 1.88, user: 1.83, sys: 0.05, mem: 456568 ko)
fingroup/perm.vo (real: 1.88, user: 1.77, sys: 0.10, mem: 482400 ko)
solvable/primitive_action.vo (real: 1.87, user: 1.83, sys: 0.04, mem: 553964 ko)
fingroup/automorphism.vo (real: 1.87, user: 1.80, sys: 0.07, mem: 472184 ko)
solvable/gfunctor.vo (real: 1.75, user: 1.68, sys: 0.06, mem: 479872 ko)
character/all_character.vo (real: 1.53, user: 1.46, sys: 0.07, mem: 740204 ko)
field/all_field.vo (real: 1.47, user: 1.39, sys: 0.08, mem: 723792 ko)
ssreflect/ssrnat.vo (real: 1.46, user: 1.39, sys: 0.06, mem: 464756 ko)
ssreflect/binomial.vo (real: 1.45, user: 1.40, sys: 0.05, mem: 472964 ko)
ssreflect/generic_quotient.vo (real: 1.40, user: 1.33, sys: 0.07, mem: 476040 ko)
solvable/all_solvable.vo (real: 1.22, user: 1.11, sys: 0.09, mem: 632408 ko)
solvable/commutator.vo (real: 1.15, user: 1.09, sys: 0.06, mem: 479524 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.08, sys: 0.06, mem: 472612 ko)
ssreflect/eqtype.vo (real: 1.12, user: 1.05, sys: 0.07, mem: 450132 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.04, sys: 0.06, mem: 465956 ko)
ssreflect/div.vo (real: 1.03, user: 0.96, sys: 0.06, mem: 446128 ko)
fingroup/presentation.vo (real: 0.54, user: 0.45, sys: 0.09, mem: 471824 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.33, sys: 0.06, mem: 449408 ko)
fingroup/all_fingroup.vo (real: 0.33, user: 0.25, sys: 0.08, mem: 465268 ko)
ssreflect/ssrfun.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 112032 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.02, mem: 140572 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 86252 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 75192 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 73240 ko)

Make the complemented lattice hierarchy symmetric w.r.t. dual: 16:59.07 (1671988ko)

1009.41user 9.53system 16:59.07elapsed 99%CPU (0avgtext+0avgdata 1671988maxresident)k
ssreflect/order.vo (real: 195.82, user: 195.51, sys: 0.31, mem: 1671988 ko)
algebra/ssrnum.vo (real: 71.00, user: 70.77, sys: 0.22, mem: 1299216 ko)
algebra/ssralg.vo (real: 59.45, user: 59.30, sys: 0.15, mem: 1353416 ko)
algebra/matrix.vo (real: 40.58, user: 40.32, sys: 0.25, mem: 1320780 ko)
character/mxrepresentation.vo (real: 28.33, user: 28.04, sys: 0.29, mem: 1021216 ko)
field/algebraics_fundamentals.vo (real: 27.11, user: 26.91, sys: 0.19, mem: 1398496 ko)
solvable/extremal.vo (real: 25.98, user: 25.83, sys: 0.15, mem: 874496 ko)
algebra/finalg.vo (real: 25.81, user: 25.66, sys: 0.14, mem: 902576 ko)
field/galois.vo (real: 23.76, user: 23.61, sys: 0.13, mem: 951944 ko)
character/classfun.vo (real: 21.45, user: 21.26, sys: 0.18, mem: 1164168 ko)
field/finfield.vo (real: 21.24, user: 21.08, sys: 0.16, mem: 1061004 ko)
character/character.vo (real: 21.08, user: 20.98, sys: 0.08, mem: 1022408 ko)
field/algC.vo (real: 20.97, user: 20.73, sys: 0.23, mem: 1208236 ko)
field/fieldext.vo (real: 18.13, user: 18.02, sys: 0.10, mem: 988928 ko)
solvable/extraspecial.vo (real: 17.66, user: 17.51, sys: 0.12, mem: 796080 ko)
algebra/interval.vo (real: 14.61, user: 14.48, sys: 0.12, mem: 1017624 ko)
algebra/mxpoly.vo (real: 14.39, user: 14.26, sys: 0.12, mem: 790924 ko)
field/closed_field.vo (real: 13.65, user: 13.50, sys: 0.15, mem: 894740 ko)
character/inertia.vo (real: 13.36, user: 13.21, sys: 0.14, mem: 892792 ko)
solvable/burnside_app.vo (real: 12.17, user: 12.05, sys: 0.11, mem: 657756 ko)
algebra/mxalgebra.vo (real: 11.98, user: 11.87, sys: 0.11, mem: 798200 ko)
algebra/poly.vo (real: 11.53, user: 11.45, sys: 0.07, mem: 762024 ko)
field/algnum.vo (real: 10.99, user: 10.92, sys: 0.06, mem: 878264 ko)
character/integral_char.vo (real: 10.70, user: 10.56, sys: 0.11, mem: 867676 ko)
algebra/vector.vo (real: 10.64, user: 10.57, sys: 0.06, mem: 826952 ko)
algebra/rat.vo (real: 10.43, user: 10.31, sys: 0.12, mem: 832624 ko)
character/vcharacter.vo (real: 10.31, user: 10.18, sys: 0.13, mem: 866768 ko)
field/falgebra.vo (real: 10.21, user: 10.09, sys: 0.11, mem: 798096 ko)
algebra/countalg.vo (real: 9.96, user: 9.88, sys: 0.08, mem: 660444 ko)
algebra/ssrint.vo (real: 9.66, user: 9.49, sys: 0.16, mem: 833196 ko)
solvable/hall.vo (real: 9.60, user: 9.53, sys: 0.06, mem: 607208 ko)
field/qfpoly.vo (real: 9.55, user: 9.39, sys: 0.14, mem: 841900 ko)
fingroup/gproduct.vo (real: 8.85, user: 8.78, sys: 0.06, mem: 562328 ko)
algebra/qpoly.vo (real: 8.85, user: 8.76, sys: 0.08, mem: 781092 ko)
solvable/maximal.vo (real: 8.84, user: 8.76, sys: 0.08, mem: 624208 ko)
field/separable.vo (real: 8.84, user: 8.71, sys: 0.12, mem: 716912 ko)
character/mxabelem.vo (real: 8.32, user: 8.26, sys: 0.06, mem: 710636 ko)
algebra/polydiv.vo (real: 8.24, user: 8.13, sys: 0.10, mem: 604472 ko)
algebra/ring_quotient.vo (real: 7.92, user: 7.82, sys: 0.10, mem: 640620 ko)
solvable/abelian.vo (real: 7.82, user: 7.68, sys: 0.13, mem: 619376 ko)
algebra/intdiv.vo (real: 7.48, user: 7.40, sys: 0.08, mem: 775556 ko)
fingroup/action.vo (real: 6.13, user: 6.02, sys: 0.09, mem: 537112 ko)
fingroup/fingroup.vo (real: 5.34, user: 5.26, sys: 0.08, mem: 550596 ko)
solvable/finmodule.vo (real: 4.86, user: 4.76, sys: 0.09, mem: 591036 ko)
solvable/center.vo (real: 4.79, user: 4.70, sys: 0.09, mem: 568112 ko)
solvable/alt.vo (real: 4.79, user: 4.70, sys: 0.08, mem: 569624 ko)
algebra/archimedean.vo (real: 4.57, user: 4.47, sys: 0.10, mem: 693632 ko)
ssreflect/bigop.vo (real: 4.15, user: 4.06, sys: 0.08, mem: 539296 ko)
ssreflect/seq.vo (real: 4.13, user: 4.03, sys: 0.10, mem: 524836 ko)
algebra/polyXY.vo (real: 4.13, user: 4.04, sys: 0.09, mem: 654312 ko)
fingroup/morphism.vo (real: 3.98, user: 3.91, sys: 0.06, mem: 490904 ko)
field/cyclotomic.vo (real: 3.95, user: 3.83, sys: 0.11, mem: 732956 ko)
ssreflect/finset.vo (real: 3.89, user: 3.80, sys: 0.08, mem: 515196 ko)
solvable/pgroup.vo (real: 3.89, user: 3.82, sys: 0.07, mem: 569248 ko)
solvable/jordanholder.vo (real: 3.70, user: 3.63, sys: 0.07, mem: 558528 ko)
all/all.vo (real: 3.69, user: 3.59, sys: 0.09, mem: 815044 ko)
solvable/cyclic.vo (real: 3.68, user: 3.60, sys: 0.08, mem: 568376 ko)
solvable/frobenius.vo (real: 3.66, user: 3.62, sys: 0.04, mem: 568528 ko)
algebra/zmodp.vo (real: 3.62, user: 3.51, sys: 0.11, mem: 588332 ko)
algebra/fraction.vo (real: 3.44, user: 3.39, sys: 0.05, mem: 561168 ko)
fingroup/quotient.vo (real: 3.39, user: 3.29, sys: 0.09, mem: 485820 ko)
ssreflect/fintype.vo (real: 3.33, user: 3.26, sys: 0.07, mem: 518072 ko)
solvable/gseries.vo (real: 2.94, user: 2.86, sys: 0.07, mem: 553068 ko)
solvable/sylow.vo (real: 2.77, user: 2.71, sys: 0.05, mem: 559180 ko)
solvable/nilpotent.vo (real: 2.53, user: 2.47, sys: 0.06, mem: 557076 ko)
ssreflect/prime.vo (real: 2.39, user: 2.31, sys: 0.07, mem: 470480 ko)
algebra/all_algebra.vo (real: 2.19, user: 2.09, sys: 0.10, mem: 699568 ko)
ssreflect/choice.vo (real: 2.05, user: 1.96, sys: 0.06, mem: 473376 ko)
fingroup/perm.vo (real: 1.90, user: 1.85, sys: 0.04, mem: 481744 ko)
ssreflect/path.vo (real: 1.89, user: 1.81, sys: 0.07, mem: 457764 ko)
ssreflect/all_ssreflect.vo (real: 1.89, user: 1.80, sys: 0.07, mem: 541436 ko)
fingroup/automorphism.vo (real: 1.87, user: 1.80, sys: 0.06, mem: 469580 ko)
solvable/primitive_action.vo (real: 1.83, user: 1.67, sys: 0.15, mem: 555368 ko)
solvable/gfunctor.vo (real: 1.82, user: 1.74, sys: 0.08, mem: 479696 ko)
character/all_character.vo (real: 1.67, user: 1.58, sys: 0.09, mem: 747052 ko)
field/all_field.vo (real: 1.59, user: 1.52, sys: 0.07, mem: 730916 ko)
ssreflect/fingraph.vo (real: 1.57, user: 1.53, sys: 0.04, mem: 454200 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.36, sys: 0.08, mem: 461804 ko)
ssreflect/generic_quotient.vo (real: 1.44, user: 1.40, sys: 0.04, mem: 477364 ko)
ssreflect/binomial.vo (real: 1.43, user: 1.39, sys: 0.04, mem: 469488 ko)
solvable/all_solvable.vo (real: 1.34, user: 1.25, sys: 0.07, mem: 617608 ko)
ssreflect/tuple.vo (real: 1.13, user: 1.07, sys: 0.05, mem: 476272 ko)
solvable/commutator.vo (real: 1.12, user: 1.06, sys: 0.05, mem: 479956 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.07, sys: 0.03, mem: 466204 ko)
ssreflect/eqtype.vo (real: 1.06, user: 0.99, sys: 0.07, mem: 449688 ko)
ssreflect/div.vo (real: 1.02, user: 0.95, sys: 0.06, mem: 447120 ko)
fingroup/presentation.vo (real: 0.57, user: 0.52, sys: 0.05, mem: 468532 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.30, sys: 0.10, mem: 448728 ko)
fingroup/all_fingroup.vo (real: 0.39, user: 0.32, sys: 0.07, mem: 466548 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.06, sys: 0.02, mem: 140720 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 112360 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.02, sys: 0.03, mem: 86108 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 75864 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 72000 ko)

Adapt order instances to the new structures: 17:48.97 (1737424ko)

1059.68user 9.16system 17:48.97elapsed 99%CPU (0avgtext+0avgdata 1737424maxresident)k
ssreflect/order.vo (real: 250.17, user: 249.90, sys: 0.25, mem: 1737424 ko)
algebra/ssrnum.vo (real: 72.09, user: 71.94, sys: 0.13, mem: 1247688 ko)
algebra/ssralg.vo (real: 59.20, user: 59.03, sys: 0.17, mem: 1352164 ko)
algebra/matrix.vo (real: 40.27, user: 40.03, sys: 0.23, mem: 1357576 ko)
character/mxrepresentation.vo (real: 28.97, user: 28.70, sys: 0.26, mem: 1032784 ko)
field/algebraics_fundamentals.vo (real: 27.14, user: 26.91, sys: 0.23, mem: 1323592 ko)
algebra/finalg.vo (real: 25.90, user: 25.81, sys: 0.09, mem: 900712 ko)
solvable/extremal.vo (real: 25.49, user: 25.33, sys: 0.16, mem: 883380 ko)
field/galois.vo (real: 23.16, user: 23.05, sys: 0.10, mem: 946232 ko)
character/classfun.vo (real: 21.84, user: 21.65, sys: 0.17, mem: 1146992 ko)
field/finfield.vo (real: 21.75, user: 21.58, sys: 0.15, mem: 1090036 ko)
field/algC.vo (real: 20.61, user: 20.43, sys: 0.17, mem: 1205164 ko)
character/character.vo (real: 20.34, user: 20.18, sys: 0.16, mem: 1009476 ko)
field/fieldext.vo (real: 17.83, user: 17.69, sys: 0.13, mem: 1034864 ko)
solvable/extraspecial.vo (real: 17.33, user: 17.22, sys: 0.11, mem: 803760 ko)
algebra/interval.vo (real: 14.68, user: 14.50, sys: 0.17, mem: 1010532 ko)
algebra/mxpoly.vo (real: 13.68, user: 13.59, sys: 0.09, mem: 797024 ko)
character/inertia.vo (real: 13.52, user: 13.38, sys: 0.14, mem: 886720 ko)
field/closed_field.vo (real: 12.21, user: 12.08, sys: 0.13, mem: 899732 ko)
solvable/burnside_app.vo (real: 11.82, user: 11.71, sys: 0.11, mem: 655184 ko)
algebra/poly.vo (real: 11.65, user: 11.52, sys: 0.13, mem: 763684 ko)
algebra/mxalgebra.vo (real: 11.22, user: 11.09, sys: 0.12, mem: 801236 ko)
field/algnum.vo (real: 11.06, user: 10.93, sys: 0.13, mem: 893732 ko)
algebra/rat.vo (real: 10.71, user: 10.52, sys: 0.18, mem: 843572 ko)
algebra/vector.vo (real: 10.63, user: 10.51, sys: 0.11, mem: 855316 ko)
character/vcharacter.vo (real: 10.47, user: 10.41, sys: 0.06, mem: 878424 ko)
character/integral_char.vo (real: 10.47, user: 10.29, sys: 0.18, mem: 891788 ko)
field/falgebra.vo (real: 10.21, user: 10.08, sys: 0.12, mem: 832576 ko)
algebra/ssrint.vo (real: 10.21, user: 10.13, sys: 0.08, mem: 863960 ko)
algebra/countalg.vo (real: 10.15, user: 10.07, sys: 0.07, mem: 660876 ko)
field/qfpoly.vo (real: 9.61, user: 9.54, sys: 0.04, mem: 842864 ko)
field/separable.vo (real: 9.22, user: 9.16, sys: 0.06, mem: 723860 ko)
solvable/hall.vo (real: 9.13, user: 9.08, sys: 0.04, mem: 609216 ko)
solvable/maximal.vo (real: 8.86, user: 8.74, sys: 0.09, mem: 624700 ko)
algebra/qpoly.vo (real: 8.81, user: 8.72, sys: 0.09, mem: 792284 ko)
algebra/polydiv.vo (real: 8.38, user: 8.28, sys: 0.09, mem: 604336 ko)
character/mxabelem.vo (real: 8.35, user: 8.19, sys: 0.15, mem: 721688 ko)
fingroup/gproduct.vo (real: 7.94, user: 7.88, sys: 0.06, mem: 562088 ko)
algebra/ring_quotient.vo (real: 7.81, user: 7.74, sys: 0.07, mem: 639764 ko)
solvable/abelian.vo (real: 7.63, user: 7.55, sys: 0.08, mem: 621544 ko)
algebra/intdiv.vo (real: 7.10, user: 7.04, sys: 0.06, mem: 785008 ko)
fingroup/action.vo (real: 6.19, user: 6.10, sys: 0.09, mem: 538468 ko)
solvable/alt.vo (real: 5.27, user: 5.11, sys: 0.14, mem: 569968 ko)
fingroup/fingroup.vo (real: 5.25, user: 5.18, sys: 0.07, mem: 548532 ko)
solvable/finmodule.vo (real: 4.90, user: 4.83, sys: 0.06, mem: 591228 ko)
algebra/archimedean.vo (real: 4.71, user: 4.61, sys: 0.09, mem: 705772 ko)
solvable/center.vo (real: 4.65, user: 4.61, sys: 0.04, mem: 568164 ko)
ssreflect/bigop.vo (real: 4.16, user: 4.07, sys: 0.08, mem: 539348 ko)
solvable/frobenius.vo (real: 4.14, user: 3.98, sys: 0.16, mem: 570808 ko)
ssreflect/seq.vo (real: 4.13, user: 4.08, sys: 0.05, mem: 524664 ko)
all/all.vo (real: 4.07, user: 3.97, sys: 0.10, mem: 815532 ko)
fingroup/morphism.vo (real: 4.03, user: 3.97, sys: 0.06, mem: 491492 ko)
algebra/polyXY.vo (real: 3.99, user: 3.94, sys: 0.05, mem: 665624 ko)
ssreflect/finset.vo (real: 3.91, user: 3.81, sys: 0.10, mem: 515648 ko)
field/cyclotomic.vo (real: 3.73, user: 3.69, sys: 0.04, mem: 741116 ko)
solvable/pgroup.vo (real: 3.71, user: 3.63, sys: 0.07, mem: 569180 ko)
algebra/zmodp.vo (real: 3.61, user: 3.53, sys: 0.08, mem: 588992 ko)
solvable/cyclic.vo (real: 3.59, user: 3.52, sys: 0.06, mem: 567824 ko)
solvable/jordanholder.vo (real: 3.57, user: 3.52, sys: 0.05, mem: 557024 ko)
fingroup/quotient.vo (real: 3.33, user: 3.19, sys: 0.11, mem: 485976 ko)
ssreflect/fintype.vo (real: 3.30, user: 3.25, sys: 0.05, mem: 518016 ko)
algebra/fraction.vo (real: 3.28, user: 3.22, sys: 0.06, mem: 561328 ko)
solvable/gseries.vo (real: 2.86, user: 2.77, sys: 0.09, mem: 553964 ko)
solvable/sylow.vo (real: 2.71, user: 2.63, sys: 0.08, mem: 560012 ko)
solvable/nilpotent.vo (real: 2.46, user: 2.39, sys: 0.07, mem: 555836 ko)
ssreflect/prime.vo (real: 2.40, user: 2.31, sys: 0.09, mem: 470472 ko)
algebra/all_algebra.vo (real: 2.16, user: 2.05, sys: 0.11, mem: 704736 ko)
ssreflect/choice.vo (real: 2.03, user: 1.98, sys: 0.04, mem: 472212 ko)
ssreflect/all_ssreflect.vo (real: 1.94, user: 1.83, sys: 0.10, mem: 552584 ko)
fingroup/perm.vo (real: 1.90, user: 1.80, sys: 0.09, mem: 482904 ko)
ssreflect/path.vo (real: 1.88, user: 1.82, sys: 0.06, mem: 457656 ko)
fingroup/automorphism.vo (real: 1.86, user: 1.82, sys: 0.04, mem: 470908 ko)
solvable/gfunctor.vo (real: 1.77, user: 1.72, sys: 0.03, mem: 479232 ko)
character/all_character.vo (real: 1.66, user: 1.54, sys: 0.12, mem: 759536 ko)
field/all_field.vo (real: 1.61, user: 1.52, sys: 0.09, mem: 743764 ko)
solvable/primitive_action.vo (real: 1.55, user: 1.47, sys: 0.08, mem: 555212 ko)
ssreflect/ssrnat.vo (real: 1.44, user: 1.39, sys: 0.05, mem: 462000 ko)
ssreflect/fingraph.vo (real: 1.42, user: 1.37, sys: 0.05, mem: 454012 ko)
ssreflect/binomial.vo (real: 1.41, user: 1.37, sys: 0.04, mem: 469184 ko)
ssreflect/generic_quotient.vo (real: 1.36, user: 1.30, sys: 0.06, mem: 476164 ko)
solvable/all_solvable.vo (real: 1.33, user: 1.26, sys: 0.07, mem: 628344 ko)
ssreflect/tuple.vo (real: 1.14, user: 1.07, sys: 0.07, mem: 472744 ko)
ssreflect/finfun.vo (real: 1.10, user: 1.04, sys: 0.06, mem: 463748 ko)
solvable/commutator.vo (real: 1.08, user: 1.01, sys: 0.07, mem: 480652 ko)
ssreflect/eqtype.vo (real: 1.06, user: 1.01, sys: 0.05, mem: 450008 ko)
ssreflect/div.vo (real: 1.03, user: 0.96, sys: 0.07, mem: 446108 ko)
fingroup/presentation.vo (real: 0.57, user: 0.51, sys: 0.04, mem: 468652 ko)
ssreflect/ssrAC.vo (real: 0.40, user: 0.33, sys: 0.06, mem: 451856 ko)
fingroup/all_fingroup.vo (real: 0.32, user: 0.25, sys: 0.07, mem: 465268 ko)
ssreflect/ssrbool.vo (real: 0.08, user: 0.07, sys: 0.01, mem: 140360 ko)
ssreflect/ssrfun.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 113348 ko)
ssreflect/ssreflect.vo (real: 0.05, user: 0.00, sys: 0.05, mem: 87084 ko)
ssreflect/ssrnotations.vo (real: 0.04, user: 0.02, sys: 0.02, mem: 76364 ko)
ssreflect/ssrmatching.vo (real: 0.04, user: 0.03, sys: 0.01, mem: 72808 ko)

Again, this is only moving things around, not adding nor removing anything.

Instead of unit. This will enable to change it to introduce involutive duals.

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

pi8027 marked this pull request as draft February 1, 2024 12:55

pi8027 added the kind: enhancement Issue or PR about addition of features. label Feb 1, 2024

pi8027 commented Feb 1, 2024

View reviewed changes

pi8027 force-pushed the hb-semilattices branch from 4d203fb to 207e36e Compare February 6, 2024 14:04

proux01 mentioned this pull request Feb 12, 2024

Preorder #1169

Open

4 tasks

pi8027 force-pushed the hb-semilattices branch from 796094d to 53685a6 Compare February 16, 2024 15:45

pi8027 force-pushed the hb-semilattices branch 2 times, most recently from 262d00d to 2a4defe Compare March 11, 2024 14:34

pi8027 commented Mar 12, 2024

View reviewed changes

pi8027 mentioned this pull request Mar 13, 2024

Various lemmas #738

Merged

2 tasks

pi8027 force-pushed the hb-semilattices branch from 8f906af to cddba38 Compare March 14, 2024 15:46

pi8027 commented Mar 14, 2024

View reviewed changes

mathcomp/ssreflect/order.v Outdated Show resolved Hide resolved

pi8027 added a commit to math-comp/multinomials that referenced this pull request Mar 15, 2024

Adapt to math-comp/math-comp#1166

fdc4929

pi8027 added a commit to pi8027/deriving that referenced this pull request Mar 15, 2024

Adapt to math-comp/math-comp#1166

d68767c

pi8027 mentioned this pull request Mar 15, 2024

Adapt to math-comp/math-comp#1166 arthuraa/deriving#28

Closed

proux01 reviewed Mar 15, 2024

View reviewed changes

mathcomp/ssreflect/order.v Outdated Show resolved Hide resolved

pi8027 added a commit to pi8027/deriving that referenced this pull request Mar 15, 2024

Adapt to math-comp/math-comp#1166

eae8fa0

pi8027 added a commit to math-comp/analysis that referenced this pull request Mar 19, 2024

Adapt to math-comp/math-comp#1166

f5059d2

pi8027 mentioned this pull request Mar 19, 2024

Adapt to math-comp/math-comp#1166 math-comp/analysis#1189

Merged

2 tasks

pi8027 force-pushed the hb-semilattices branch from 8fc5b08 to eaede30 Compare March 19, 2024 16:18

pi8027 force-pushed the hb-semilattices branch from eaede30 to 5631187 Compare March 19, 2024 16:43

proux01 added this to the 2.3.0 milestone Apr 18, 2024

pi8027 added 7 commits April 18, 2024 16:52

Minor cleanup

3e3b042

These changes should not have any semantic impact.

Add subCountType and subFinType instances on copies of n.-tuple T in …

34bfeb5

…order.v

Group factories

98b8116

This commit only moves things around for clarity, it doesn't add nor remove anything.

Move dual instances

22d70f1

Again this is only moving things around, not adding nor removing anything.

Generalize some order lemmas to bPOrderType, tPOrderType, and tDistrL…

05334dd

…atticeType

proux01 force-pushed the hb-semilattices branch from ac092f5 to af8ec1d Compare April 18, 2024 16:12

proux01 approved these changes Apr 19, 2024

View reviewed changes

proux01 mentioned this pull request Apr 19, 2024

Adapt to math-comp/math-comp#1166 math-comp/multinomials#88

Merged

proux01 pushed a commit to math-comp/analysis that referenced this pull request Apr 19, 2024

Adapt to math-comp/math-comp#1166

974b51c

affeldt-aist pushed a commit to affeldt-aist/analysis that referenced this pull request Apr 19, 2024

Adapt to math-comp/math-comp#1166

73dc130

pi8027 added a commit to math-comp/multinomials that referenced this pull request Apr 19, 2024

Merge pull request #88 from math-comp/hb-semilattices

05ce627

Adapt to math-comp/math-comp#1166

pi8027 force-pushed the hb-semilattices branch from af8ec1d to 3a3216e Compare April 22, 2024 13:47

pi8027 added 3 commits April 22, 2024 16:01

Move lemmas around

0029238

Again, this is only moving things around, not adding nor removing anything.

Add a proper type for order displays

9b5af50

Instead of unit. This will enable to change it to introduce involutive duals.

Make dual_display involutive

edd3218

pi8027 force-pushed the hb-semilattices branch from 3a3216e to 9e17282 Compare April 22, 2024 14:02

pi8027 and others added 6 commits April 23, 2024 13:23

Update the header documentation of order.v

27d839d

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

Make dual involutive

f41bf8f

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

Add semilattice structures

6f59959

Make the complemented lattice hierarchy symmetric w.r.t. dual

31a25d2

Adapt order instances to the new structures

f457da3

CHANGELOG

ca2eda6

pi8027 force-pushed the hb-semilattices branch from 9e17282 to ca2eda6 Compare April 23, 2024 11:24

proux01 merged commit c8a578d into master Apr 24, 2024
103 checks passed

CohenCyril approved these changes Apr 24, 2024

View reviewed changes

proux01 deleted the hb-semilattices branch April 24, 2024 11:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Semilattices and definitional duality #1166

Semilattices and definitional duality #1166

pi8027 commented Feb 1, 2024 •

edited

pi8027 Feb 1, 2024

proux01 Apr 19, 2024

pi8027 Mar 12, 2024

proux01 Apr 19, 2024

proux01 Apr 21, 2024

pi8027 Apr 22, 2024

pi8027 Apr 22, 2024

proux01 Apr 22, 2024

pi8027 Mar 12, 2024

proux01 Apr 19, 2024

pi8027 Mar 12, 2024

proux01 Apr 19, 2024

pi8027 commented Mar 15, 2024

proux01 commented Mar 15, 2024

pi8027 commented Mar 15, 2024

pi8027 commented Mar 19, 2024

proux01 commented Mar 19, 2024

pi8027 commented Mar 19, 2024

pi8027 commented Mar 19, 2024

proux01 commented Mar 19, 2024

proux01 commented Mar 19, 2024

proux01 left a comment

proux01 Apr 19, 2024

proux01 Apr 19, 2024

proux01 commented Apr 20, 2024

	(* FIXME: lemmas in the following section should hold for any porderType *)
	(* FIXME: some lemmas in the following section should hold for any porderType *)

Semilattices and definitional duality #1166

Semilattices and definitional duality #1166

Conversation

pi8027 commented Feb 1, 2024 • edited

Motivation for this change

Overlay PRs

Things done/to do

Other TODOs (to be done in separate PRs)

Compatibility with MathComp 1.X

Automatic note to reviewers

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pi8027 commented Mar 15, 2024

proux01 commented Mar 15, 2024

pi8027 commented Mar 15, 2024

pi8027 commented Mar 19, 2024

proux01 commented Mar 19, 2024

pi8027 commented Mar 19, 2024

pi8027 commented Mar 19, 2024

proux01 commented Mar 19, 2024

proux01 commented Mar 19, 2024

proux01 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

proux01 commented Apr 20, 2024

pi8027 commented Feb 1, 2024 •

edited