gapt/gapt/gapt.proofs/gapt.proofs.lk/gapt.proofs.lk.rules/InductionCase

InductionCase

gapt.proofs.lk.rules.InductionCase

case class InductionCase(proof: LKProof, constructor: Const, hypotheses: Seq[SequentIndex], eigenVars: Seq[Var], conclusion: SequentIndex)

Proof that a given data type constructor c preserves a formula F:

                                (π)
F(x,,1,,), F(x,,2,,), ..., F(x,,n,,), Γ :- Δ, F(c(x,,1,,,...,x,,n,,,y,,1,,,...,y,,n,,))

The variables x,,i,, and y,,i,, are eigenvariables; x,,i,, are the eigenvariables of the same type as the inductive data type, y,,i,, are the other arguments of the constructor c. They can come in any order in the constructor.

Value parameters

conclusion: Index of F(c(x,,1,,,...,x,,n,,,y,,1,,,...,y,,n,,))
constructor: The constructor c of the inductive data type that we're considering.
eigenVars: The eigenvariables of this case: x,,1,,, ..., x,,n,,, y,,1,,, ..., y,,n,, (these need to correspond to the order in c)
hypotheses: Indices of F(x,,1,,), ..., F(x,,n,,)
proof: The LKProof ending in the sequent of this case.

Attributes

Source: InductionCase.scala
Graph
Supertypes: trait Serializable

trait Product

trait Equals

class Object

trait Matchable

class Any
Show all