Re: [isabelle] Goedel's Proof




Thanks, John, it was an error in transcription. Here are the first three.I hope the html marking will also be transmitted ..

//--------------------------------------
// 1. Proposition
// x is divisible by y
//--------------------------------------
BOOL divisible(NAT x, NAT y) {
NAT z;
for (z=1;(z<=y);z++)
  if (x==y*z)
    return TRUE;
return FALSE;}

//--------------------------------------
// 2. Proposition
// x is a prime number
//--------------------------------------
BOOL Prim(NAT x) {
NAT z;
for (z=1;(z<=x);z++)
  if (z!=1)
    if (z!=x)
      return TRUE;
return FALSE;}

//--------------------------------------
// 3. Function
// the n-th prime number contained in x
//--------------------------------------
NAT Pr2(NAT n, NAT x) {
NAT y;
if (n==0) return 0;
else {
  n
=0;
  for
(y=1;(y<=x);y++) {
    n
=n+1;
    if
(Prim(y))
      if (divisible(x,y))
        if (y>Pr2(n-1,x))
          return
y;

  }
}

return 0;}


Best Regards
Jens Doll


Am 26.06.2012 09:08, schrieb John Wickerson:
I think that "z" should be an "i" :) john


Attachment: Goedel.jpg
Description: JPEG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.