GradedStrictMonotoneSequenceSchema

gapt.examples.GradedStrictMonotoneSequenceSchema
object GradedStrictMonotoneSequenceSchema extends TacticsProof

Attributes

Graph
Supertypes
class TacticsProof
class TacticsProof0
class Object
trait Matchable
class Any
Self type

Members list

Value members

Inherited methods

def main(args: Array[String]): Unit

Attributes

Inherited from:
TacticsProof

Concrete fields

val ChiSc: LKProof
val ChiScm: LKProof
val chi1Bc: LKProof
val chi1Bcm: LKProof
val chi1Sc: LKProof
val chi1Scm: LKProof
val chiBc: LKProof
val chiBcm: LKProof
val deltaBc: LKProof
val deltaSc: LKProof
val epsilonBc: LKProof
val epsilonSc: LKProof
val esChi: Sequent[Formula]
val esChi1Bc: Sequent[(String, Formula)]
val esChi1Bcm: Sequent[(String, Formula)]
val esChi1Sc: Sequent[(String, Formula)]
val esChi1Scm: Sequent[(String, Formula)]
val esChiBc: Sequent[(String, Formula)]
val esChiBcm: Sequent[(String, Formula)]
val esChiSc: Sequent[(String, Formula)]
val esChiScm: Sequent[(String, Formula)]
val esDelta: Sequent[Formula]
val esDeltaBc: Sequent[(String, Formula)]
val esDeltaSc: Sequent[(String, Formula)]
val esEpsilon: Sequent[Formula]
val esEpsilonBc: Sequent[(String, Formula)]
val esEpsilonSc: Sequent[(String, Formula)]
val esMu: Sequent[Formula]
val esNu: Sequent[Formula]
val esNu1Bc: Sequent[(String, Formula)]
val esNu2Bc: Sequent[(String, Formula)]
val esNuBc: Sequent[(String, Formula)]
val esNuSc: Sequent[(String, Formula)]
val esOmega: Sequent[Formula]
val esOmegaBc: Sequent[(String, Formula)]
val esOmegaSc: Sequent[(String, Formula)]

The Parameter N is the size of the range The parameter K is the number of jumps The Parameter M is the number of equivalences in a plateau

The Parameter N is the size of the range The parameter K is the number of jumps The Parameter M is the number of equivalences in a plateau

Attributes

val esPhi: Sequent[Formula]
val esPhiBc: Sequent[(String, Formula)]
val esPhiBc1: Sequent[(String, Formula)]
val esPhiBc1m: Sequent[(String, Formula)]
val esPhiBcm: Sequent[(String, Formula)]
val esPhiSc: Sequent[(String, Formula)]
val esPhiSc1: Sequent[(String, Formula)]
val esPhiSc1m: Sequent[(String, Formula)]
val esPhiScm: Sequent[(String, Formula)]
val esPsi: Sequent[Formula]
val esPsiBc: Sequent[(String, Formula)]
val esPsiSc: Sequent[(String, Formula)]
val esTheta: Sequent[Formula]
val esThetaBc: Sequent[(String, Formula)]
val esThetaSc: Sequent[(String, Formula)]
val esXi: Sequent[Formula]
val esXiBc: Sequent[(String, Formula)]
val esXiSc: Sequent[(String, Formula)]
val esZeta: Sequent[Formula]
val esZetaBc: Sequent[(String, Formula)]
val esZetaSc: Sequent[(String, Formula)]
val esmuBc: Sequent[(String, Formula)]
val esmuSc: Sequent[(String, Formula)]
val muBc: LKProof
val muSc: LKProof
val nu1Bc: LKProof
val nu2Bc: LKProof
val nuBc: LKProof
val nuSc: LKProof
val omegaBc: LKProof
val omegaSc: LKProof
val phiBc: LKProof
val phiBc1: LKProof
val phiBc1m: LKProof
val phiBcm: LKProof
val phiSc: LKProof
val phiSc1: LKProof
val phiSc1m: LKProof
val phiScm: LKProof
val psiBc: LKProof
val psiSc: LKProof
val thetaBc: LKProof
val thetaSc: LKProof
val xiBc: LKProof
val xiSc: LKProof
val zetaBc: LKProof
val zetaSc: LKProof

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0