//-------------------------------------------
// The following functions
// have been derived from
// Goedels 46+ propositions.
//
// "On Formally Undecidable Propositions of
// Principa Mathematics and Related Systems"
// by Kurt Goedel, Vienna
//
// Translated by B. Meltzer
// Dover Publications 1962, 1992
//
//-------------------------------------------
// EXISTS(v,low,high,cond,res)
// := find first v>=low and v<=high
// which satisfies cond andreturn res
//
// FORALL(v,low,high,cond)
// := do next check for all v>=low and v<=high
//
//-------------------------------------------
// (c) Context IT GmbH, Ahrensburg, Germany
// Web: http://www.cococo.de
//
// Version: 0.8 July, 7th 2012
// Modified: NN
//
// Please send bug reports and feature
// requests to [email protected]
//-------------------------------------------
#include "defs.nat.h"
#include "propositions.h"
//--------------------------------------
// I.1 Axiom
//--------------------------------------
NATFUN1(AxiomI1,n,"there is no predecessor for ZERO","Es gibt keinen Vorgaenger fuer NULL")
EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
RESULT(FALSE)
FIN
//--------------------------------------
// I.2 Axiom
//--------------------------------------
NATFUN2(AxiomI2,n,m,"if fx = fy then x = y","wenn fx = fy dann ist x = y")
EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
RESULT(FALSE)
FIN
//--------------------------------------
// I.3 Axiom
//--------------------------------------
NATFUN1(AxiomI3,n,"Ex x2(0) && Forall(x1,x2(x1)>x2(f x1)) \n"
" => Forall(x1,x2(x1))",
"Ex x2(0) && Forall(x1,x2(x1)>x2(f x1)) \n"
" => Forall(x1,x2(x1))")
EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
RESULT(FALSE)
FIN
//--------------------------------------
// II.1 Axiom
//--------------------------------------
NATFUN2(AxiomII1,p,q,"p or q => p", "p or q => p")
CASE(Dis(p,q),Neg(p))
RESULT(FALSE)
FIN
//--------------------------------------
// II.2 Axiom
//--------------------------------------
NATFUN2(AxiomII2,p,q,"p => p or q","p => p or q")
CASE(p,Dis(p,q))
RESULT(FALSE)
FIN
//--------------------------------------
// II.3 Axiom
//--------------------------------------
NATFUN2(AxiomII3,p,q,"p or q => p","p or q => p")
CASE(Dis(p,q),Dis(q,p));
RESULT(FALSE)
FIN
//--------------------------------------
// II.1 Axiom
//--------------------------------------
NATFUN3(AxiomII4,p,q,r,"(p => q) => (r or p => r or q)","(p => q) => (r or p => r or q)")
CASE(Dis(p,q),p)
RESULT(FALSE)
FIN
//--------------------------------------
// III.1 Axiom
//--------------------------------------
NATFUN2(AxiomIII1,a,c,"Forall(v,a) => Subst(a v c)","Forall(v,a) => Subst(a v c)")
CASE(Dis(a,c),a)
RESULT(FALSE)
FIN
//--------------------------------------
// III.2 Axiom
//--------------------------------------
NATFUN2(AxiomIII2,a,c,"Forall(v,b or a) => b or Forall(v,a)","Forall(v,b or a) => b or Forall(v,a)")
CASE(Dis(a,c),a)
RESULT(FALSE)
FIN
//--------------------------------------
// IV.1 Axiom
//--------------------------------------
NATFUN2(AxiomIV1,a,c,"Ex u Forall(v,u(v)=a)","Ex u Forall(v,u(v)=a)")
CASE(Dis(a,c),a)
RESULT(FALSE)
FIN
//--------------------------------------
// V.1 Axiom
//--------------------------------------
NATFUN2(AxiomV1,a,c,"Forall(x1,(x2(x1) = y2(x1) => x2 = y2))","Forall(x1,(x2(x1) = y2(x1) => x2 = y2))")
CASE(Dis(a,c),a)
RESULT(FALSE)
FIN
//--------------------------------------
// 1. Proposition
//--------------------------------------
BOOLFUN2(divisible,x,y,"x is divisible by y","x ist durch y teilbar")
EXISTS(z,TWO,x,Eq(x,Mul(y,z)),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 2. Proposition
//--------------------------------------
BOOLFUN1(Prim,x,"x is a prime number","x ist eine Primzahl")
CASE(Eq(x,ONE),TRUE)
EXISTS(z,TWO,x,And(Ne(z,x),divisible(x,z)),FALSE);
RESULT(TRUE)
FIN
//--------------------------------------
// 3. Function (2 parameters)
//--------------------------------------
NATFUN2(Pr2,n,x,"the n-th prime number contained in x\n (also see Pr1, Pr2)"
,"die n'te Primzahl die in x enthalten ist\n (siehe auch Pr1, Pr2)")
CASE(Eq(n,ZERO),ZERO)
EXISTS(y,Add(Pr2(Sub(n,ONE),x),ONE),x,And(Prim(y),divisible(x,y)),y);
RESULT(ZERO)
FIN
//--------------------------------------
// 4. Function
//--------------------------------------
NATFUN1(Fac,n,"faculty of n","Fakultaet von n")
CASE(Eq(n,ZERO),ZERO)
CASE(Eq(n,ONE),ONE)
RESULT(Mul(n,Fac(Sub(n,ONE))))
FIN
//--------------------------------------
// 5. Function (1 parameter)
//--------------------------------------
NATFUN1(Pr1,n,"n-th prime number\n(also see Pr1, Pr2)",
"die n'te Primzahl\n(siehe auch Pr1, Pr2)")
CASE(Eq(n,ZERO),ZERO)
EXISTS(y,Add(Pr1(Sub(n,ONE)),ONE),Add(Fac(Pr1(Sub(n,ONE))),ONE),Prim(y),y);
RESULT(ZERO)
FIN
//--------------------------------------
// 6. Function
//--------------------------------------
NATFUN2(Gl,n,x,"n-th term of a series of numbers assigned to x",
"der n'te Term einer Folge von Zahlen die x zugewiesen sind")
NAT pp=Pr2(n,x);
EXISTS(y,ONE,x,And(divisible(x,Pow(pp,y)),Not(divisible(x,Pow(pp,Add(y,ONE))))),y);
RESULT(ZERO)
FIN
//--------------------------------------
// 7. Function
//--------------------------------------
NATFUN1(l,x,"length a series of numbers of assigned to x",
"Laenge einer Folge von Zahlen die x zugewiésen sind")
EXISTS(y,ONE,x,And(Gt(Pr2(y,x),ZERO),Eq(Pr2(Add(y,ONE),x),ZERO)),y);
RESULT(ZERO)
FIN
//--------------------------------------
// 8. Function
//--------------------------------------
// 8.1
BOOLFUN2(Join1,x,z,"auxiliary","hilfsweise")
EXISTS(n,ONE,l(x),Ne(Gl(n,z),Gl(n,x)),FALSE);
RESULT(TRUE)
FIN
// 8.2
BOOLFUN3(Join2,x,y,z,"auxiliary","hilfsweise")
EXISTS(n,ZERO,l(y),Ne(Gl(Add(n,l(x)),z),Gl(n,y)),FALSE);
RESULT(TRUE)
FIN
// 8.
NATFUN2(Join,x,y,"join together two finite series of numbers",
"verkette zwei endliche Folgen von Zahlen")
EXISTS(z,ONE,Pow(Pr1(Add(l(x),l(y))),Add(x,y)),And(Join1(x,z),Join2(x,y,z)),z);
RESULT(ZERO)
FIN
//--------------------------------------
// 9. Function
//--------------------------------------
NATFUN1(R,x,"a series of numbers with a single element x",
"eine Zahlenfolge mit nur einem Element x")
RESULT(Pow(TWO,x))
FIN
//--------------------------------------
// 10. Function
//--------------------------------------
NATFUN1(E,x,"bracketing of a a series of numbers",
"Klammerung eier Zahlenfolge")
RESULT(Join(R(ELEVEN),Join(x,R(THIRTEEN))))
FIN
//--------------------------------------
// 11. Function (2 parameters)
//--------------------------------------
BOOLFUN2(Var2,n,x,"x is a variable of n-th type\n (also see Var1, Var2)",
"x ist eine Variable vom n'ten Typ\n (siehe auch Var1, Var2)")
CASE(Eq(n,ZERO),FALSE)
EXISTS(z,Add(THIRTEEN,ONE),x,And(Prim(z),Eq(x,Pow(z,n))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 12. Proposition (1 parameter)
//--------------------------------------
BOOLFUN1(Var1,x,"x is a variable","x ist eine Variable")
EXISTS(n,ONE,x,Var2(n,x),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 13. Function
//--------------------------------------
NATFUN1(Neg,x,"negation of x","Negation von x")
RESULT(Join(R(FIVE),E(x)))
FIN
//--------------------------------------
// 14. Function
//--------------------------------------
NATFUN2(Dis,x,y,"disjunction of x, y","Disjunktion von x, y")
RESULT(Join(E(x),Join(R(SEVEN),E(y))))
FIN
//--------------------------------------
// 15. Function
//--------------------------------------
NATFUN2(Gen,x,y,"generalization of y by means of variable x",
"Generalisierung von y durch die Variable x")
RESULT(Join(R(x),Join(R(NINE),E(y))))
FIN
//--------------------------------------
// 16. Function
//--------------------------------------
NATFUN2(N,n,x,"n-fold prefixing of the sign f(succ) before x",
"n-facher Praefix des Zeichens f(succ) vor x")
CASE(Eq(n,ZERO),x)
RESULT(Join(R(THREE),N(Sub(n,ONE),x)))
FIN
//--------------------------------------
// 17. Function
//--------------------------------------
NATFUN1(Z,n,"number sign for number n","Zahlenzeichen fuer n")
RESULT(N(n,R(ONE)))
FIN
//--------------------------------------
// 18. Proposition (1 parameter)
//--------------------------------------
BOOLFUN1(Typ1,x,"x is a sign of first type\n (also see Typ1, Typ2)",
"x ist ein Zeichen ersten Typs\n (siehe auch Typ1, Typ2)")
FORALL(n,ONE,x)
EXISTS(m,ONE,x,Or(Eq(m,ONE),And(Var2(ONE,m),Eq(x,N(n,R(m))))),TRUE);
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 19. Proposition (2 parameters)
//--------------------------------------
BOOLFUN2(Typ2,n,x,"x is a sign of n-th type\n (also see Typ1, Typ2)",
"x ist ein ZEichen n-ten Typs\n (siehe auch Typ1, Typ2)")
CASE(Eq(n,ONE),Typ1(x))
EXISTS(v,ONE,x,And(Var2(n,v),Eq(x,R(v))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 20. Proposition
//--------------------------------------
BOOLFUN1(Elf,x,"x is an elementary type",
"x ist ein elementaarer Typ")
FORALL(y,ONE,x)
FORALL(z,ONE,x)
EXISTS(n,ONE,x,And(Typ2(n,y),And(Typ2(Add(n,ONE),z),Eq(x,Join(z,E(y))))),TRUE)
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 21. Proposition
//--------------------------------------
BOOLFUN3(Op,x,y,z,"nn","NN")
CASE(Eq(x,Neg(y)),TRUE)
CASE(Eq(x,Dis(y,z)),TRUE)
EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 22. Proposition
//--------------------------------------
BOOLFUN1(FR,x,"x is a series of formula \n"
" where each formula is either elementary\n"
" or it arises from negation, disjunction,\n"
" and generalization",
"x is eine Folge von Formeln \n"
" in der jede Formel entweder elementar ist\n"
" oder aus Negation, Disjunktion,\n"
" und Generalisierung besteht")
FORALL(n,ONE,x)
CASE(And(Lt(ZERO,n),Le(n,l(x))),Elf(Gl(n,x)))
FORALL(p,ONE,n)
EXISTS(q,ONE,n,Op(Gl(n,x),Gl(p,x),Gl(q,x)),TRUE);
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 23. Proposition
//--------------------------------------
BOOLFUN1(Form,x,"x is a formula","x ist eine Formel")
EXISTS(n,ONE,Pow(Pr1(Pow(l(x),TWO)),Mul(x,Pow(l(x),TWO))),And(FR(n),Eq(x,Gl(l(n),n))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 24. Proposition
//--------------------------------------
BOOLFUN3(Geb,v,n,x,"variable v is bound at n-th place in x",
"Variable v ist an n-ter Stelle in x gebunden")
CASE(Not(And(Var1(v),Form(x))),FALSE)
FORALL(a,ONE,x)
FORALL(b,ONE,x)
EXISTS(c,ONE,x,And(Eq(x,Join(a,Join(Gen(v,b),c))),And(Form(b),And(Le(Add(l(a),ONE),n),Le(n,Add(l(a),l(Gen(v,b))))))),TRUE);
ENDFOR
ENDFOR
FIN
//--------------------------------------
// 25. Proposition (3 parameters)
//--------------------------------------
BOOLFUN3(Fr3,v,n,x,"variable v is free at n-th place in x\n (also see Fr2, Fr3)",
"Variable v ist an n-ter Stelle frei in x\n (siehe auch Fr2, Fr3)")
RESULT(And(Var1(v),And(Form(x),And(Eq(v,Gl(n,x)),And(Le(n,l(x)),Geb(v,n,x))))))
FIN
//--------------------------------------
// 26. Proposition (2 parameters)
//--------------------------------------
BOOLFUN2(Fr2,v,x,"v occurs in x as a free variable\n (also see Fr2, Fr3)",
"v ist eine freie Variable aus x\n (siehe auch Fr2, Fr3)")
EXISTS(n,ONE,l(x),Fr3(v,n,x),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 27. Proposition
//--------------------------------------
NATFUN3(Su,x,n,y,"substitute y in place of the n-th term of x",
"ersetze y an der Stelle des n-ten Terms in x")
FORALL(z,ONE,Pr1(Add(Pow(l(x),l(y)),Add(x,y))))
FORALL(u,ONE,x)
EXISTS(v,ONE,x,And(Eq(x,Join(u,Join(R(Gl(n,x)),v))),And(Eq(z,Join(u,Join(y,v))),Eq(n,Add(l(u),ONE)))),v)
ENDFOR
ENDFOR
RESULT(ZERO)
FIN
//--------------------------------------
// 28. Function
//--------------------------------------
NATFUN3(St,k,v,x,"(k+1)-th place in x at which v is free in x, 0 else",
"die (k+1)-te Stelle in x an der v frei ist, 0 sonst")
FORALL(n,ONE,l(x))
EXISTS(p,Add(n,ONE),l(x),And(Eq(k,ZERO),And(Fr3(v,n,x),Fr3(v,p,x))),n);
ENDFOR
FORALL(n,ONE,St(k,v,x))
EXISTS(p,Add(n,ONE),St(k,v,x),And(Fr3(v,n,x),Fr3(v,p,x)),n);
ENDFOR
RESULT(ZERO)
FIN
//--------------------------------------
// 29. Function
//--------------------------------------
NATFUN2(A,v,x,"number of places at which v is free in x",
"Anzahl der Stellen an denen v frei in x ist")
EXISTS(n,ONE,l(x),Eq(St(n,v,x),ZERO),n);
RESULT(ZERO)
FIN
//--------------------------------------
// 30. Function
//--------------------------------------
NATFUN4(Sb4,k,x,v,y,"substitute ...\n (also see Sb3, Sb4)",
"ersetze ...\n (siehe auch Sb3, Sb4)")
CASE(Eq(k,ZERO),x)
RESULT(Su(Sb4(Sub(k,ONE),x,v,y),St(k,v,x),y))
FIN
//--------------------------------------
// 31. Function
//--------------------------------------
NATFUN3(Sb3,x,v,y,"substitute x by v in y\n (also see Sb3, Sb4)",
"ersetze x durch v in y\n (siehe auch Sb3, Sb4)")
RESULT(Sb4(A(v,x),x,v,y))
FIN
//--------------------------------------
// 32a. Function
//--------------------------------------
NATFUN2(Imp,x,y,"implication",
"Implikation")
RESULT(Dis(Neg(x),y))
FIN
//--------------------------------------
// 32b. Function
//--------------------------------------
NATFUN2(Con,x,y,"conjunction",
"Konjunktion")
RESULT(Neg(Dis(Neg(x),Neg(y))))
FIN
//--------------------------------------
// 32c. Function
//--------------------------------------
NATFUN2(Aeq,x,y,"equivalence",
"Aequivalenz")
RESULT(Con(Imp(x,y),Imp(y,x)))
FIN
//--------------------------------------
// 32d. Function
//--------------------------------------
NATFUN2(Ex,v,y,"exists","Es gibt")
RESULT(Neg(Gen(v,Neg(y))))
FIN
//--------------------------------------
// 33. Function
//--------------------------------------
NATFUN2(Th,n,x,"n-th type lift of x",
"n-ter Typ von x")
FORALL(y,ONE,Pow(x,Pow(x,n)))
EXISTS(k,ONE,l(x),And(Le(Gl(k,x),THIRTEEN),Eq(Gl(k,y),Gl(k,x))),y);
EXISTS(k,ONE,l(x),And(Gt(Gl(k,x),THIRTEEN),Eq(Gl(k,y),Join(Gl(k,x),Pow(Pr2(ONE,Gl(k,x)),n)))),y);
ENDFOR
RESULT(ZERO)
FIN
//--------------------------------------
// 34. Proposition
//--------------------------------------
BOOLFUN1(Z_Ax,x,"axioms I(1) to I(3)",
"Axiome I(1) bis I(3)")
CASE(Eq(x,z1),TRUE)
CASE(Eq(x,z2),TRUE)
CASE(Eq(x,z3),TRUE)
RESULT(FALSE)
FIN
//--------------------------------------
// 35. Proposition
//--------------------------------------
BOOLFUN2(A1_Ax,n,x,"formula derived by substituton",
"Formel die durch Substitution abgeleitet wurde")
EXISTS(y,ONE,x,And(Form(y),Eq(x,Imp(Dis(y,y),y))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 36. Proposition
//--------------------------------------
BOOLFUN1(A_Ax,x,"formula derived by substituton",
"Formel die durch Substitution abgeleitet wurde")
CASE(A1_Ax(ONE,x),TRUE)
CASE(A1_Ax(TWO,x),TRUE)
CASE(A1_Ax(THREE,x),TRUE)
CASE(A1_Ax(FOUR,x),TRUE)
RESULT(FALSE)
FIN
//--------------------------------------
// 37. Proposition
//--------------------------------------
BOOLFUN3(Q,z,y,v,"z contains no variable bound in y at position where v is free",
"z enthaelt keine Variable in y an der Position wo v frei ist")
FORALL(n,ONE,l(y))
FORALL(m,ONE,l(z))
EXISTS(w,ONE,z,And(Eq(w,Gl(m,y)),And(Geb(w,n,y),Fr3(v,n,y))),TRUE);
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 38. Proposition
//--------------------------------------
BOOLFUN1(L1_Ax,x,"--> bug in paper Sb(v z)??\n"
" x is a formula derived from the axiom schema III,1 by substitution",
"--> Fehler in Papier Sb(v z) ??\n"
"x ist eine aus dem Axiomem III,1 durch Substitution abgeleitete Formel")
FORALL(v,ONE,x)
FORALL(y,ONE,x)
FORALL(z,ONE,x)
EXISTS(n,ONE,x,And(Var2(n,v),And(Typ2(n,z),And(Form(y),
And(Q(z,y,v),Eq(x,Imp(Gen(v,y),Sb3(n,v,z))))))),TRUE);
ENDFOR
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 39. Proposition
//--------------------------------------
BOOLFUN1(L2_Ax,x,"x is a formula derived from the axiom schema III,2 by substitution",
"x ist eine aus dem Axiomem III,2 durch Substitution abgeleitete Formel")
FORALL(v,ONE,x)
FORALL(q,ONE,x)
EXISTS(p,ONE,x,And(Var1(v),And(Form(p),And(Fr2(v,p),And(Form(q),
Eq(x,Gen(v,Imp(Dis(p,q),Dis(p,Gen(v,q))))))))),TRUE);
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 40. Proposition
//--------------------------------------
BOOLFUN1(R_Ax,x,"x is a formula derived from the axiom schema IV,1 by substitution",
"x ist eine aus dem Axiomem IV,1 durch Substitution abgeleitete Formel")
FORALL(u,ONE,x)
FORALL(v,ONE,x)
FORALL(y,ONE,x)
EXISTS(n,ONE,x,And(Var2(n,v),And(Var2(Add(n,ONE),u),And(Fr2(u,y),
And(Form(y),Eq(x,Ex(u,Gen(v,Aeq(Join(R(u),E(R(v))),y)))))))),TRUE);
ENDFOR
ENDFOR
ENDFOR
RESULT(FALSE)
FIN
//--------------------------------------
// 41. Proposition
//--------------------------------------
BOOLFUN1(M_Ax,x,"tbd","offen")
EXISTS(n,ONE,x,(Eq(x,Th(n,z4))),TRUE);
RESULT(FALSE)
FIN
//--------------------------------------
// 42. Proposition
//--------------------------------------
BOOLFUN1(Ax,x,"x is an axiom","x ist ein Axiom")
CASE(Z_Ax(x),TRUE)
CASE(A1_Ax(ONE,x),TRUE)
CASE(L1_Ax(x),TRUE)
CASE(L2_Ax(x),TRUE)
CASE(R_Ax(x),TRUE)
CASE(M_Ax(x),TRUE)
RESULT(FALSE)
FIN
//--------------------------------------
// 43. Proposition
//--------------------------------------
BOOLFUN3(Fl,x,y,z,"x is an immediate consequence of y and z",
"x ist unmittelbare Folgerung von y und z")
CASE(Imp(z,x),TRUE)
EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
FIN
//--------------------------------------
// 44. Proposition
//--------------------------------------
BOOLFUN1(Bw,x,"x is a proof schema","x ist ein Beweisschema")
FORALL(n,ZERO,l(x))
FORALL(p,ZERO,n)
EXISTS(q,ZERO,n,And(And(Not(Ax(Gl(n,x))),Gt(l(x),ZERO)),Fl(Gl(n,x),Gl(p,x),Gl(q,x))),FALSE);
ENDFOR
ENDFOR
RESULT(TRUE)
FIN
//--------------------------------------
// 45. Proposition
//--------------------------------------
BOOLFUN2(B,x,y,"x is a proof of the formula y",
"x beweist Formal y")
RESULT(And(Bw(x),Eq(Gl(l(x),x),y)))
FIN
//--------------------------------------
// 46. Proposition
//--------------------------------------
BOOLFUN1(Bew,x,"x is a provable formula\n"
" (cannot be asserted that it is recursive)",
"x ist eine beweisbare Formel\n"
" (es kann nicht gesagt werden ob diese Funktion rekursiv ist)")
EXISTS(y,ZERO,Add(y,ONE),B(y,x),TRUE); //y+1==TRUE, INFINITE
RESULT(FALSE)
FIN
//--------------------------------------
//
// Additional Functions
//
//
//--------------------------------------
// Primetwin
//--------------------------------------
NATFUN1(Primetwin,n,"p, p+2 are primes, p>n\n"
" (unknown if there are infinitely many)",
"p, p+2 sind Primzahlen, p>n\n"
" (unbekannt ob es fuer alle n terminiert)")
EXISTS(p,n,Mul(n,ELEVEN),And(Prim(p),Prim(Add(p,TWO))),Pair(p,Add(p,TWO)));
RESULT(ZERO)
FIN
//--------------------------------------
// Goldbach
//--------------------------------------
NATFUN1(Goldbach,n," p+q=n where p,q are primes\n"
" (Goldbach's conjecture)",
" p+q=n wobei p,q Primzahlen sind"
" (Goldbachs Behauptung)")
CASE(Ne(Mod(n,TWO),ZERO),ZERO)
FORALL(q,ONE,Sub(n,ONE))
EXISTS(p,ONE,Sub(n,ONE),And(Eq(Add(p,q),n),And(Prim(q),Prim(p))),Pair(p,q))
ENDFOR
CASE(TRUE,ZERO)
FIN
//--------------------------------------
// Collatz
//--------------------------------------
NATFUN1(Collatz,n,"sequence of either n/2 or 3*n+1\n"
" (a proof of convergence is unknown)",
"eine Zahlenfolge mit n/2 oder 3*n+1 als Nachfolger"
" (ein Beweis fuer die Konvergenz existiert nicht)")
CASE(Le(n,ONE),n)
CASE(Eq(Mod(n,TWO),ZERO),Collatz(Div(n,TWO)))
RESULT(Collatz(Add(Mul(n,THREE),ONE)))
FIN
//--------------------------------------
// Fermat
//--------------------------------------
NATFUN1(Fermat,n,"Forall n, n mod 4 = 1\n"
" ex x,y x*x+y*y = n",
"Forall n, n mod 4 = 1\n"
" ex x,y x*x+y*y = n")
CASE(Ne(Mod(n,FOUR),ONE),ZERO)
FORALL(x,TWO,Sub(n,ONE))
EXISTS(y,TWO,Sub(x,ONE),Eq(Add(Mul(x,x),Mul(y,y)),n),y)
ENDFOR
FIN
//--------------------------------------
// End of this Source
//--------------------------------------
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
