---------------> The definition of the formula cGC.



  Def-01: The natural numbers collectively is a language model
          [for the language of arithmetic L(PA)] of which the
          universe U is non-finite.

  Def-02: prime(x)  <-> Ax1x2[(S0<x /\ (x=x1*x2)) -> ((x1=S0 /\ x=x2) \/ (x2=S0 /\ x=x1))]
  Def-03a: even1(x) <-> Ey[x=y+y]
  Def-03b: even2(x) <-> Ey[x=2*y]
  Def-03c: even(x)  <-> (even1(x) \/ even2(x))

  Def-04a: odd1(x)  <-> Ey[x=(y+y+S0)]
  Def-04b: odd2(x)  <-> Ey[x=((SS0*y)+S0)]
  Def-04c: odd(x)   <-> (odd1(x) \/ odd2(x))

  Def-05a: GC(x)    <-> (even(x) /\ (SS0<x)) -> Ep1p2[prime(p1) /\ prime(p2) /\ (x=p1+p2)]

  Def-05b: aGC(x)   <-> (even(x) /\ (SS0<x)) -> Ap1p2[prime(p1) /\ prime(p2) /\ (p1+p2<x \/ x<p1+p2)]

  Def-06a: Assuming a P(x), the statement "There are infinitely many
           examples of P" would be symbolized as '(I)P(*)' and defined
           as:

           (I)P(*) <-> Ex[P(x)] /\ AxEy[P(x) -> (P(y) /\ Ez(y = x + Sz))]

           This is called I-form (Inductive) of infinity expression.

  Def-06b: Assuming a P(x), the statement "There are infinitely many
           examples of P" could also be symbolized as '(aI)P(*)' and
           defined as:

           (aI)P(*) <-> Ex[P(x)] /\ AxEy[P(x) -> (P(y) /\ (x < y))]

           This is called aI-form (anti-Inductive) of infinity
           expression.

  Def-06c: P(*) <-> ((I)P(*) \/ (aI)P(*))

           This is the general form of infinity expression about the
           naturals.

  Def-07:  cGC <-> aGC(*)