gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.sequence/FactorialFunctionEqualityExampleProof2

FactorialFunctionEqualityExampleProof2

gapt.examples.sequence.FactorialFunctionEqualityExampleProof2
object FactorialFunctionEqualityExampleProof2 extends ProofSequence

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def ASSO(x: FOLTerm, y: FOLTerm, z: FOLTerm): FOLAtom
def apply(n: Int): LKProof
def endSequent(n: Int): HOLSequent
def f(x: FOLTerm): FOLTerm
def f0: FOLAtom
def fST(x: FOLTerm): FOLAtom
def g(x: FOLTerm, y: FOLTerm): FOLTerm
def g0(x: FOLTerm): FOLAtom
def gST(x: FOLTerm, y: FOLTerm): FOLAtom
def m(x: FOLTerm, y: FOLTerm): FOLTerm
def s(x: FOLTerm): FOLTerm
def target(x: FOLTerm): FOLAtom
def uL(x: FOLTerm): FOLAtom
def uR(x: FOLTerm): FOLAtom

Inherited methods

def name: String

Attributes

Inherited from:
ProofSequence

Concrete fields

val alpha: FOLVar
val beta: FOLVar
val gamma: FOLVar
val nu: FOLVar
val one: FOLTerm
val w: FOLVar
val x: FOLVar
val y: FOLVar
val z: FOLVar
val zero: FOLConst
Generated with