gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.examples/gapt.examples.prime/furstenberg

furstenberg

gapt.examples.prime.furstenberg
case class furstenberg(k: Int) extends PrimeDefinitions

Furstenberg's topological proof of the infinitude of primes.

furstenberg(k) proves that there are more than k primes.

Attributes

Source
furstenberg.scala
Graph
Supertypes
trait Serializable
trait Product
trait Equals
class TacticsProof
class Object
trait Matchable
class Any
Show all
Known subtypes
object furstenberg3.type

Members list

Value members

Concrete methods

def RQ(n: Int): LKProof

Attributes

Source
furstenberg.scala
def lambda(n: Int): LKProof

Attributes

Source
furstenberg.scala
def psi2Right(n: Int): LKProof

Attributes

Source
furstenberg.scala
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

Source
furstenberg.scala

Inherited methods

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

Attributes

Inherited from:
TacticsProof
Source
TacticsProof.scala
def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product

Concrete fields

val FQ: LKProof

Attributes

Source
furstenberg.scala
val FR: LKProof

Attributes

Source
furstenberg.scala
val Pi_1: LKProof

Attributes

Source
furstenberg.scala
val compCompProof: LKProof

Attributes

Source
furstenberg.scala
val deMorgan1: LKProof

Attributes

Source
furstenberg.scala
val infiniteSubset: LKProof

Attributes

Source
furstenberg.scala
val intersectionOpen: LKProof

Attributes

Source
furstenberg.scala
val openClosedProof: LKProof

Attributes

Source
furstenberg.scala
val pgt0: LKProof

Attributes

Source
furstenberg.scala
val phi2: LKProof

Attributes

Source
furstenberg.scala
val progClosed: LKProof

Attributes

Source
furstenberg.scala
val proof: LKProof

Attributes

Source
furstenberg.scala
val psi1: LKProof

Attributes

Source
furstenberg.scala
val psi1Left: LKProof

Attributes

Source
furstenberg.scala
val psi1Right: LKProof

Attributes

Source
furstenberg.scala
val psi2: LKProof

Attributes

Source
furstenberg.scala
val singletonFinite: LKProof

Attributes

Source
furstenberg.scala
val unionClosed: LKProof

Attributes

Source
furstenberg.scala

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0
Source
TacticsProof.scala
implicit def spliceNum(i: Int): Splice[Expr]

Attributes

Inherited from:
PrimeDefinitions
Source
PrimeDefinitions.scala
Generated with