gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.prime/furstenberg3

furstenberg3

gapt.examples.prime.furstenberg3
object furstenberg3 extends furstenberg

Attributes

Graph
Supertypes
class furstenberg
trait Serializable
trait Product
trait Equals
class TacticsProof
class TacticsProof0
class Object
trait Matchable
class Any
Show all
Self type

Members list

Value members

Inherited methods

def RQ(n: Int): LKProof

Attributes

Inherited from:
furstenberg
def lambda(n: Int): LKProof

Attributes

Inherited from:
furstenberg
def main(args: Array[String]): Unit

Attributes

Inherited from:
TacticsProof
def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product
def psi2Right(n: Int): LKProof

Attributes

Inherited from:
furstenberg
def varrho2(n: Int): LKProof

Proof of x ∈ S[n] :- ∃y ( y ∈ P[n] ∧ x ∈ ν(0,y) )

Proof of x ∈ S[n] :- ∃y ( y ∈ P[n] ∧ x ∈ ν(0,y) )

Attributes

Inherited from:
furstenberg

Inherited fields

val FQ: LKProof

Attributes

Inherited from:
furstenberg
val FR: LKProof

Attributes

Inherited from:
furstenberg
val Pi_1: LKProof

Attributes

Inherited from:
furstenberg
val compCompProof: LKProof

Attributes

Inherited from:
furstenberg
val deMorgan1: LKProof

Attributes

Inherited from:
furstenberg
val infiniteSubset: LKProof

Attributes

Inherited from:
furstenberg
val intersectionOpen: LKProof

Attributes

Inherited from:
furstenberg
val openClosedProof: LKProof

Attributes

Inherited from:
furstenberg
val pgt0: LKProof

Attributes

Inherited from:
furstenberg
val phi2: LKProof

Attributes

Inherited from:
furstenberg
val progClosed: LKProof

Attributes

Inherited from:
furstenberg
val proof: LKProof

Attributes

Inherited from:
furstenberg
val psi1: LKProof

Attributes

Inherited from:
furstenberg
val psi1Left: LKProof

Attributes

Inherited from:
furstenberg
val psi1Right: LKProof

Attributes

Inherited from:
furstenberg
val psi2: LKProof

Attributes

Inherited from:
furstenberg
val singletonFinite: LKProof

Attributes

Inherited from:
furstenberg
val singletonNonempty: LKProof

Attributes

Inherited from:
furstenberg
val unionClosed: LKProof

Attributes

Inherited from:
furstenberg

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0
implicit def spliceNum(i: Int): Splice[Expr]

Attributes

Inherited from:
PrimeDefinitions
Generated with