JavaScript is disabled for your browser. Some features of this site may not work without it.

eCommons will be completely unavailable from 8:00am April 4 until 5:00pm April 5, 2018, for software upgrades. Thank you for your patience during this planned service interruption.
Please contact us at ecommons-admin@cornell.edu if you have questions or concerns.

## The Fundamental Theorem of Arithmetic in PL/CV2

#####
**Author**

Constable, Robert L.

#####
**Abstract**

This document is a section of formal elementary number theory leading up to a complete proof of the fundamental theorem of arithmetic. On the way to this result a large number of simple facts about integer division, prime numbers, greatest common divisors, and the product function, $\prod_{i=1}^{m}a(i)$, are developed. The entire section is written in the formal logic of PL/CV2, and the proof was checked by the PL/CV2 Proof Checker on an IBM 370/168. Readers familiar with the syntax of a high level programming language, like PL/I, and accustomed to highly symbolic mathematical proofs should be able to read this document as a specimen of extremely formal and rigorous mathematics. The following remarks about PL/CV2 notation will simplify reading. 1. The *PROCESS line indicates the beginning of PL/I executable text, the *THEOREM line indicates the beginning of purely declarative text. 2. All proof text is written between PL/I comment delimiters of the form /*/...*/ or /#...#/ depending on context. 3. For the built-in PL/I functions ABS, MOD, SIGN, MAX, MIN, EXP, DIVISION (/) only the properties of the functions are listed, in Section 0 called BUILT-IN FUNCTIONS. No proofs of these properties are supplied (because the operations are provided by the system). Thus proved propositions appear starting in Section 1 (at line 0036). 4. In the listing the negation sign is written ^, thus B ^= 0 reads "B not equal to zero". The PL/I symbol for "or" is the vertical bar, thus line 0037 TRI : B less than 0|B=0|B greater than 0 is labeled by TRI (for trichotomy) and means B is less than or equal to 0 or greater than 0. The justification... BY ARITH... indicates that the conclusion follows from simple arithmetic reasoning, provided by the system, from the list of hypotheses. 5. Every PL/CV2 procedure, such as LOG at line 0049, begins with an ASSUME statement, telling what is assumed about the input, and with an ATTAIN statement telling what will be proved about it. Also every procedure is proved to terminate. In the case of recursive procedures, the termination proof begins with the line ARBITRARY (integer variable) WHERE (conditon) (see line 0053). It is proved that this integer variable decreases on any recursive call.

#####
**Date Issued**

1980-06#####
**Publisher**

Cornell University

#####
**Subject**

computer science; technical report

#####
**Previously Published As**

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR80-424

#####
**Type**

technical report