Skip to content

Add axiom that guarantees that L is always increases #2

@konard

Description

@konard

https://github.com/linksplatform/Theory/blob/19c09c5185ab7fcd80a40cfd9f724082e7c52777/associative_proofs/net_defs.v#L24-L26

Add axiom that guarantees that L is always increases.

Variable L : Type.
Variable LS : L -> L.
Variable greater : L -> L -> bool.

Axiom LS_increases : forall n : L, greater n (LS n) = true.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions