FDL > PVS > Prelude > lex2 : Theory

PVS-2.4 prelude.pvs

 lex2 provides a lexical ordering for pairs of natural numbers.
 This illustrates the use of ordinals.

lex2 : THEORY
BEGIN

i: VAR nat

j: VAR nat

m: VAR nat

n: VAR nat

%%(TCC) lex2_TCC1: OBLIGATION

%%(TCC) lex2_TCC2: OBLIGATION

%%(TCC) lex2_TCC3: OBLIGATION

%%(TCC) lex2_TCC4: OBLIGATION

%%(TCC) lex2_TCC5: OBLIGATION

%%(TCC) lex2_TCC6: OBLIGATION

%%(TCC) lex2_TCC7: OBLIGATION

%%(TCC) lex2_TCC8: OBLIGATION

lex2(m, n): ordinal = IF m = 0 THEN IF n = 0 THEN zero ELSE add(n, zero, zero) ENDIF ELSE IF n = 0 THEN add(m, add(1, zero, zero), zero) ELSE add(m, add(1, zero, zero), add(n, zero, zero)) ENDIF ENDIF;

lex2 lt: LEMMA (lex2(i, j) < lex2(m, n)) = ((i < m) OR ((i = m) AND (j < n)))

END lex2