SequentialInductionAxioms
Generates sequential induction axioms.
Value parameters
- fsel
-
The formula of a sequent for which induction axioms are generated.
- vsel
-
The variables for which an induction axiom is generated.
Attributes
- Source
- SequentialInductionAxioms.scala
- Graph
-
- Supertypes
-
trait Serializabletrait Producttrait Equalstrait AxiomFactoryclass Objecttrait Matchableclass AnyShow all
Members list
Value members
Concrete methods
Computes sequential induction axioms for a sequent.
Computes sequential induction axioms for a sequent.
Value parameters
- ctx
-
The context defining types, constants, etc.
- sequent
-
The sequent for which the axioms are generated.
Attributes
- Returns
-
Failure if the one of the given variables is not of inductive type. Otherwise a list of induction axioms of the form: ∀A∀{X < x}( IC(x,c,,1,,) ∧ ... ∧ IC(x,c,,l,,) -> ∀x∀{X > x}∀{X'}F ), where the input variables are X the input formula is of the form F' = ∀{X U X'}F FV(F') = A x in X {X < x} and {X > x} are subsets of X containing all variables with index smaller/greater than the index of x.
- Definition Classes
- Source
- SequentialInductionAxioms.scala
Attributes
Attributes
Attributes
Attributes
Attributes
Inherited methods
Attributes
- Inherited from:
- AxiomFactory
- Source
- AxiomFactory.scala
An iterator over the names of all the elements of this product.
An iterator over the names of all the elements of this product.
Attributes
- Inherited from:
- Product
- Source
- Product.scala
An iterator over all the elements of this product.
An iterator over all the elements of this product.
Attributes
- Returns
-
in the default implementation, an
Iterator[Any] - Inherited from:
- Product
- Source
- Product.scala