Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Metatheorem resolving all consequences of Equation1571 #341

Merged
merged 16 commits into from
Oct 7, 2024
Merged

Metatheorem resolving all consequences of Equation1571 #341

merged 16 commits into from
Oct 7, 2024

Commits on Oct 4, 2024

  1. added theorem for fully right-associating operation trees in associat… 

    …ive magmas (semigroups)
    @franklindyer
    franklindyer committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    ff72e10 View commit details
    Browse the repository at this point in the history

  2. added Equation1571_implies_Equation3167 as another example usage of A… 

    …ssocFullyRightAssociate
    @franklindyer
    franklindyer committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    7cab02e View commit details
    Browse the repository at this point in the history

  3. added definition of FreeSemigroup and instanced it into Magma

    @franklindyer
    franklindyer committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    d0d4a28 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2024

  1. added (currently nonworking) first attempt at insertion sort reductio… 

    …n on commutative semigroups
    @franklindyer
    franklindyer committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    27e53bd View commit details
    Browse the repository at this point in the history

  2. completed insertion sort proof for commutative semigroups

    @franklindyer
    franklindyer committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    8a764db View commit details
    Browse the repository at this point in the history

  3. renamed FreeMonoid.lean to FreeSemigroup.lean and cleaned up inconsis… 

    …tent naming
    @franklindyer
    franklindyer committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    57951d1 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2024

  1. changed import from FreeMonoid to FreeSemigroup

    @franklindyer
    franklindyer committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    2d4d339 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. finished general-purpose prover that should knock out all consequence… 

    …s of Equation1571
    @franklindyer
    franklindyer committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    b5d45fe View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into free-monoid-theory

    @franklindyer
    franklindyer authored Oct 7, 2024
    Configuration menu
    Copy the full SHA
    56800c5 View commit details
    Browse the repository at this point in the history

  3. removed 'foo'

    @franklindyer
    franklindyer committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    a68732e View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'refs/remotes/origin/free-monoid-theory'… 

    … into free-monoid-theory
    @franklindyer
    franklindyer committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    544ed7c View commit details
    Browse the repository at this point in the history

  5. Merge branch 'main' into free-monoid-theory

    @pitmonticone
    pitmonticone authored Oct 7, 2024
    Configuration menu
    Copy the full SHA
    8bae82e View commit details
    Browse the repository at this point in the history

  6. golf proofs

    @pitmonticone
    pitmonticone committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    ee8d70d View commit details
    Browse the repository at this point in the history

  7. Merge branch 'free-monoid-theory' of https://github.com/franklindyer/… 

    …equational_theories into pr/341
    @pitmonticone
    pitmonticone committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    abd63fb View commit details
    Browse the repository at this point in the history

  8. Update Subgraph.lean

    @pitmonticone
    pitmonticone committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    0cc5fe6 View commit details
    Browse the repository at this point in the history

  9. Update Subgraph.lean

    @pitmonticone
    pitmonticone committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    3ca9ebb View commit details
    Browse the repository at this point in the history