gapt-examples
API
Generated with
gapt-examples/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

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

Members list

Value members

Concrete methods

def RQ(n: Int): LKProof
def lambda(n: Int): LKProof
def psi2Right(n: Int): LKProof
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 methods

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

Concrete fields

val FQ: LKProof
val FR: LKProof
val Pi_1: LKProof
val compCompProof: LKProof
val deMorgan1: LKProof
val infiniteSubset: LKProof
val intersectionOpen: LKProof
val openClosedProof: LKProof
val pgt0: LKProof
val phi2: LKProof
val progClosed: LKProof
val proof: LKProof
val psi1: LKProof
val psi1Left: LKProof
val psi1Right: LKProof
val psi2: LKProof
val singletonFinite: LKProof
val singletonNonempty: LKProof
val unionClosed: LKProof

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

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

Attributes

Inherited from:
PrimeDefinitions
Generated with