Skip to content

Prove proof constraint independence #442

Open
Open
Prove proof constraint independence#442
Labels
enhancementEnhancement of existing featuresnew featureAddition of new featuresquestionFurther information is requested
@berpeti

Description

@berpeti
berpeti
opened on Nov 12, 2024

Suppose we have a matching logic proof, which existentially generalises over x. If we know that x is a fresh variable, prove that we can construct an equivalent proof with existentially generalises over y, which is also a fresh variable.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementEnhancement of existing featuresnew featureAddition of new featuresquestionFurther information is requested

    Type

    No type

    Fields

    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