## File: entries.tex

package info (click to toggle)
hol88 2.02.19940316-35
 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613 \chapter{ML Functions in the arith Library}\input{entries-intro}\DOC{ARITH\_CONV} \TYPE {\small\verb%ARITH_CONV : conv%}\egroup \SYNOPSIS Partial decision procedure for a subset of linear natural number arithmetic. \DESCRIBE {\small\verb%ARITH_CONV%} is a partial decision procedure for Presburger natural arithmetic. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the relations {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%} and the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, {\small\verb%==>%}, {\small\verb%=%} (if-and-only-if), {\small\verb%!%} (forall') and {\small\verb%?%} (there exists'). Products of two expressions which both contain variables are not included in the subset, but the function {\small\verb%SUC%} which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation. {\small\verb%ARITH_CONV%} further restricts the subset as follows: when the formula has been put in prenex normal form it must contain only one kind of quantifier, that is the quantifiers must either all be universal (forall') or all existential. Variables may appear free (unquantified) provided any quantifiers that do appear in the prenex normal form are universal; free variables are taken as being implicitly universally quantified so mixing them with existential quantifiers would violate the above restriction. Given a formula in the permitted subset, {\small\verb%ARITH_CONV%} attempts to prove that it is equal to {\small\verb%T%} (true). For universally quantified formulae the procedure only works if the formula would also be true of the non-negative rationals; it cannot prove formulae whose truth depends on the integral properties of the natural numbers. The procedure is also incomplete for existentially quantified formulae, but in this case there is no rule-of-thumb for determining whether the procedure will work. The function features a number of preprocessors which extend the coverage beyond the subset specified above. In particular, natural number subtraction and conditional statements are allowed. Another permits substitution instances of universally quantified formulae to be accepted. Note that Boolean-valued variables are not allowed. \FAILURE The function can fail in two ways. It fails if the argument term is not a formula in the specified subset, and it also fails if it is unable to prove the formula. The failure strings are different in each case. However, the function may announce that it is unable to prove a formula that one would expect it to reject as being outside the subset. This is due to it looking for substitution instances; it has generalised the formula so that the new formula is in the subset but is not valid. \EXAMPLE A simple example containing a free variable: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV "m < SUC m";; |- m < (SUC m) = T \end{verbatim} } \noindent A more complex example with subtraction and universal quantifiers, and which is not initially in prenex normal form: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV # "!m p. p < m ==> !q r. (m < (p + q) + r) ==> ((m - p) < q + r)";; |- (!m p. p < m ==> (!q r. m < ((p + q) + r) ==> (m - p) < (q + r))) = T \end{verbatim} } \noindent Two examples with existential quantifiers: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV "?m n. m < n";; |- (?m n. m < n) = T #ARITH_CONV "?m n. (2 * m) + (3 * n) = 10";; |- (?m n. (2 * m) + (3 * n) = 10) = T \end{verbatim} } \noindent An instance of a universally quantified formula involving a conditional statement and subtraction: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV # "((p + 3) <= n) ==> (!m. ((m EXP 2 = 0) => (n - 1) | (n - 2)) > p)";; |- (p + 3) <= n ==> (!m. ((m EXP 2 = 0) => n - 1 | n - 2) > p) = T \end{verbatim} } \noindent Failure due to mixing quantifiers: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV "!m. ?n. m < n";; evaluation failed ARITH_CONV -- formula not in the allowed subset \end{verbatim} } \noindent Failure because the truth of the formula relies on the fact that the variables cannot have fractional values: {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV "!m n. ~(SUC (2 * m) = 2 * n)";; evaluation failed ARITH_CONV -- cannot prove formula \end{verbatim} } \SEEALSO NEGATE_CONV, EXISTS_ARITH_CONV, FORALL_ARITH_CONV, INSTANCE_T_CONV, PRENEX_CONV, SUB_AND_COND_ELIM_CONV. \ENDDOC \DOC{ARITH\_FORM\_NORM\_CONV} \TYPE {\small\verb%ARITH_FORM_NORM_CONV : conv%}\egroup \SYNOPSIS Normalises an unquantified formula of linear natural number arithmetic. \DESCRIBE {\small\verb%ARITH_FORM_NORM_CONV%} converts a formula of natural number arithmetic into a disjunction of conjunctions of less-than-or-equal-to inequalities. The arithmetic expressions are only allowed to contain natural number constants, numeric variables, addition, the {\small\verb%SUC%} function, and multiplication by a constant. The formula must not contain quantifiers, but may have disjunction, conjunction, negation, implication, equality on Booleans (if-and-only-if), and the natural number relations: {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%}. The formula must not contain products of two expressions which both contain variables. The inequalities in the result are normalised so that each variable appears on only one side of the inequality, and each side is a linear sum in which any constant appears first followed by products of a constant and a variable. The variables are ordered lexicographically, and if the coefficient of the variable is {\small\verb%1%}, the product of {\small\verb%1%} and the variable appears in the term rather than the variable on its own. \FAILURE The function fails if the argument term is not a formula in the specified subset. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #ARITH_FORM_NORM_CONV "m < n";; |- m < n = (1 + (1 * m)) <= (1 * n) #ARITH_FORM_NORM_CONV # "(n < 4) ==> ((n = 0) \/ (n = 1) \/ (n = 2) \/ (n = 3))";; |- n < 4 ==> (n = 0) \/ (n = 1) \/ (n = 2) \/ (n = 3) = 4 <= (1 * n) \/ (1 * n) <= 0 /\ 0 <= (1 * n) \/ (1 * n) <= 1 /\ 1 <= (1 * n) \/ (1 * n) <= 2 /\ 2 <= (1 * n) \/ (1 * n) <= 3 /\ 3 <= (1 * n) \end{verbatim} } \USES Useful in constructing decision procedures for linear arithmetic. \ENDDOC \DOC{COND\_ELIM\_CONV} \TYPE {\small\verb%COND_ELIM_CONV : conv%}\egroup \SYNOPSIS Eliminates conditional statements from a formula. \DESCRIBE This function moves conditional statements up through a term and if at any point the branches of the conditional become Boolean-valued the conditional is eliminated. If the term is a formula, only an abstraction can prevent a conditional being moved up far enough to be eliminated. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #COND_ELIM_CONV "!f n. f ((SUC n = 0) => 0 | (SUC n - 1)) < (f n) + 1";; |- (!f n. (f((SUC n = 0) => 0 | (SUC n) - 1)) < ((f n) + 1)) = (!f n. (~(SUC n = 0) \/ (f 0) < ((f n) + 1)) /\ ((SUC n = 0) \/ (f((SUC n) - 1)) < ((f n) + 1))) #COND_ELIM_CONV "!f n. (\m. f ((m = 0) => 0 | (m - 1))) (SUC n) < (f n) + 1";; |- (!f n. ((\m. f((m = 0) => 0 | m - 1))(SUC n)) < ((f n) + 1)) = (!f n. ((\m. ((m = 0) => f 0 | f(m - 1)))(SUC n)) < ((f n) + 1)) \end{verbatim} } \USES Useful as a preprocessor to decision procedures which do not allow conditional statements in their argument formula. \SEEALSO SUB_AND_COND_ELIM_CONV. \ENDDOC \DOC{DISJ\_INEQS\_FALSE\_CONV} \TYPE {\small\verb%DISJ_INEQS_FALSE_CONV : conv%}\egroup \SYNOPSIS Proves a disjunction of conjunctions of normalised inequalities is false, provided each conjunction is unsatisfiable. \DESCRIBE {\small\verb%DISJ_INEQS_FALSE_CONV%} converts an unsatisfiable normalised arithmetic formula to false. The formula must be a disjunction of conjunctions of less-than-or-equal-to inequalities. The inequalities must have the following form: Each variable must appear on only one side of the inequality and each side must be a linear sum in which any constant appears first followed by products of a constant and a variable. On each side the variables must be ordered lexicographically, and if the coefficient of the variable is {\small\verb%1%}, the {\small\verb%1%} must appear explicitly. \FAILURE Fails if the formula is not of the correct form or is satisfiable. The function will also fail on certain unsatisfiable formulae due to incompleteness of the procedure used. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #DISJ_INEQS_FALSE_CONV # "(1 * n) <= ((1 * m) + (1 * p)) /\ # ((1 * m) + (1 * p)) <= (1 * n) /\ # (5 + (4 * n)) <= ((3 * m) + (1 * p)) \/ # 2 <= 0";; |- (1 * n) <= ((1 * m) + (1 * p)) /\ ((1 * m) + (1 * p)) <= (1 * n) /\ (5 + (4 * n)) <= ((3 * m) + (1 * p)) \/ 2 <= 0 = F \end{verbatim} } \SEEALSO ARITH_FORM_NORM_CONV. \ENDDOC \DOC{EXISTS\_ARITH\_CONV} \TYPE {\small\verb%EXISTS_ARITH_CONV : conv%}\egroup \SYNOPSIS Partial decision procedure for non-universal Presburger natural arithmetic. \DESCRIBE {\small\verb%EXISTS_ARITH_CONV%} is a partial decision procedure for formulae of Presburger natural arithmetic which are in prenex normal form and have all variables existentially quantified. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the relations {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%} and the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, {\small\verb%==>%}, {\small\verb%=%} (if-and-only-if), {\small\verb%!%} (forall') and {\small\verb%?%} (there exists'). Products of two expressions which both contain variables are not included in the subset, but the function {\small\verb%SUC%} which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation. Given a formula in the specified subset, the function attempts to prove that it is equal to {\small\verb%T%} (true). The procedure is incomplete; it is not able to prove all formulae in the subset. \FAILURE The function can fail in two ways. It fails if the argument term is not a formula in the specified subset, and it also fails if it is unable to prove the formula. The failure strings are different in each case. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #EXISTS_ARITH_CONV "?m n. m < n";; |- (?m n. m < n) = T #EXISTS_ARITH_CONV "?m n. (2 * m) + (3 * n) = 10";; |- (?m n. (2 * m) + (3 * n) = 10) = T \end{verbatim} } \SEEALSO NEGATE_CONV, FORALL_ARITH_CONV, ARITH_CONV. \ENDDOC \DOC{FORALL\_ARITH\_CONV} \TYPE {\small\verb%FORALL_ARITH_CONV : conv%}\egroup \SYNOPSIS Partial decision procedure for non-existential Presburger natural arithmetic. \DESCRIBE {\small\verb%FORALL_ARITH_CONV%} is a partial decision procedure for formulae of Presburger natural arithmetic which are in prenex normal form and have all variables either free or universally quantified. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the relations {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%} and the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, {\small\verb%==>%}, {\small\verb%=%} (if-and-only-if), {\small\verb%!%} (forall') and {\small\verb%?%} (there exists'). Products of two expressions which both contain variables are not included in the subset, but the function {\small\verb%SUC%} which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation. Given a formula in the specified subset, the function attempts to prove that it is equal to {\small\verb%T%} (true). The procedure only works if the formula would also be true of the non-negative rationals; it cannot prove formulae whose truth depends on the integral properties of the natural numbers. \FAILURE The function can fail in two ways. It fails if the argument term is not a formula in the specified subset, and it also fails if it is unable to prove the formula. The failure strings are different in each case. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FORALL_ARITH_CONV "m < SUC m";; |- m < (SUC m) = T #FORALL_ARITH_CONV "!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)";; |- (!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)) = T #FORALL_ARITH_CONV "!m n. ~(SUC (2 * m) = 2 * n)";; evaluation failed FORALL_ARITH_CONV -- cannot prove formula \end{verbatim} } \SEEALSO NEGATE_CONV, EXISTS_ARITH_CONV, ARITH_CONV, ARITH_FORM_NORM_CONV, DISJ_INEQS_FALSE_CONV. \ENDDOC \DOC{INSTANCE\_T\_CONV} \TYPE {\small\verb%INSTANCE_T_CONV : ((term -> term list) -> conv -> conv)%}\egroup \SYNOPSIS Function which allows a proof procedure to work on substitution instances of terms that are in the domain of the procedure. \DESCRIBE This function generalises a conversion that is used to prove formulae true. It does this by first replacing any syntactically unacceptable subterms with variables. It then attempts to prove the resulting generalised formula and if successful it re-instantiates the variables. The first argument should be a function which computes a list of subterms of a term which are syntactically unacceptable to the proof procedure. This function should include in its result any variables that do not appear in other subterms returned. The second argument is the proof procedure to be generalised; this should be a conversion which when successful returns an equation between the argument formula and {\small\verb%T%} (true). \FAILURE Fails if either of the applications of the argument functions fail, or if the conversion does not return an equation of the correct form. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FORALL_ARITH_CONV "!f m (n:num). (m < (f n)) ==> (m <= (f n))";; evaluation failed FORALL_ARITH_CONV -- formula not in the allowed subset #INSTANCE_T_CONV non_presburger_subterms FORALL_ARITH_CONV # "!f m (n:num). (m < (f n)) ==> (m <= (f n))";; |- (!f m n. m < (f n) ==> m <= (f n)) = T \end{verbatim} } \ENDDOC \DOC{is\_prenex} \TYPE {\small\verb%is_prenex : (term -> bool)%}\egroup \SYNOPSIS Determines whether a formula is in prenex normal form. \DESCRIBE This function returns true if the term it is given as argument is in prenex normal form. If the term is not a formula the result will be true provided there are no nested Boolean expressions involving quantifiers. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #is_prenex "!x. ?y. x \/ y";; true : bool #is_prenex "!x. x ==> (?y. x /\ y)";; false : bool \end{verbatim} } \USES Useful for determining whether it is necessary to apply a prenex normaliser to a formula before passing it to a function which requires the formula to be in prenex normal form. \SEEALSO PRENEX_CONV. \ENDDOC \DOC{is\_presburger} \TYPE {\small\verb%is_presburger : (term -> bool)%}\egroup \SYNOPSIS Determines whether a formula is in the Presburger subset of arithmetic. \DESCRIBE This function returns true if the argument term is a formula in the Presburger subset of natural number arithmetic. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the natural number relations {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%} and the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, {\small\verb%==>%}, {\small\verb%=%} (if-and-only-if), {\small\verb%!%} (forall') and {\small\verb%?%} (there exists'). Products of two expressions which both contain variables are not included in the subset, but the function {\small\verb%SUC%} which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation. This function also considers subtraction to be part of the subset. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #is_presburger "!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p";; true : bool #is_presburger "!m n p q. m < (n * p) /\ (n * p) < q ==> m < q";; false : bool #is_presburger "(m <= n) ==> !p. (m < SUC(n + p))";; true : bool #is_presburger "(m + n) - m = n";; true : bool \end{verbatim} } \USES Useful for determining whether a decision procedure for Presburger arithmetic is applicable to a term. \SEEALSO non_presburger_subterms, FORALL_ARITH_CONV, EXISTS_ARITH_CONV, is_prenex. \ENDDOC \DOC{NEGATE\_CONV} \TYPE {\small\verb%NEGATE_CONV : (conv -> conv)%}\egroup \SYNOPSIS Function for negating the operation of a conversion that proves a formula to be either true or false. \DESCRIBE This function negates the operation of a conversion that proves a formula to be either true or false. For example, if {\small\verb%conv%} proves {\small\verb%"t"%} to be equal to {\small\verb%"T"%} then {\small\verb%NEGATE_CONV conv%} will prove {\small\verb%"~t"%} to be {\small\verb%"F"%}. \FAILURE Fails if the application of the conversion to the negation of the formula does not yield either {\small\verb%"T"%} or {\small\verb%"F"%}. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #ARITH_CONV "!n. 0 <= n";; |- (!n. 0 <= n) = T #NEGATE_CONV ARITH_CONV "~(!n. 0 <= n)";; |- ~(!n. 0 <= n) = F #NEGATE_CONV ARITH_CONV "?n. ~(0 <= n)";; |- (?n. ~0 <= n) = F \end{verbatim} } \ENDDOC \DOC{non\_presburger\_subterms} \TYPE {\small\verb%non_presburger_subterms : (term -> term list)%}\egroup \SYNOPSIS Computes the subterms of a term that are not in the Presburger subset of arithmetic. \DESCRIBE This function computes a list of subterms of a term that are not in the Presburger subset of natural number arithmetic. All numeric variables in the term are included in the result. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the natural number relations {\small\verb%<%}, {\small\verb%<=%}, {\small\verb%=%}, {\small\verb%>=%}, {\small\verb%>%} and the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, {\small\verb%==>%}, {\small\verb%=%} (if-and-only-if), {\small\verb%!%} (forall') and {\small\verb%?%} (there exists'). Products of two expressions which both contain variables are not included in the subset, so such products will appear in the result list. However, the function {\small\verb%SUC%} which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation. This function also considers subtraction to be part of the subset. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #non_presburger_subterms "!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p";; ["m"; "n"; "p"] : term list #non_presburger_subterms "!m n p q. m < (n * p) /\ (n * p) < q ==> m < q";; ["m"; "n * p"; "q"] : term list #non_presburger_subterms "(m + n) - m = f n";; ["m"; "n"; "f n"] : term list \end{verbatim} } \SEEALSO INSTANCE_T_CONV, is_presburger. \ENDDOC \DOC{PRENEX\_CONV} \TYPE {\small\verb%PRENEX_CONV : conv%}\egroup \SYNOPSIS Puts a formula into prenex normal form. \DESCRIBE This function puts a formula into prenex normal form, and in the process splits any Boolean equalities (if-and-only-if) into two implications. If there is a Boolean-valued subterm present as the condition of a conditional, the subterm will be put in prenex normal form, but quantifiers will not be moved out of the condition. Some renaming of variables may take place. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRENEX_CONV "!m n. (m <= n) ==> !p. (m < SUC(n + p))";; |- (!m n. m <= n ==> (!p. m < (SUC(n + p)))) = (!m n p. m <= n ==> m < (SUC(n + p))) #PRENEX_CONV "!p. (!m. m >= p) = (p = 0)";; |- (!p. (!m. m >= p) = (p = 0)) = (!p m. ?m'. (m' >= p ==> (p = 0)) /\ ((p = 0) ==> m >= p)) #PRENEX_CONV "!m. (((m = 0) ==> (!n. m <= n)) => 0 | m) + m = m";; |- (!m. (((m = 0) ==> (!n. m <= n)) => 0 | m) + m = m) = (!m. ((!n. (m = 0) ==> m <= n) => 0 | m) + m = m) \end{verbatim} } \USES Useful as a preprocessor to decision procedures which require their argument formula to be in prenex normal form. \SEEALSO is_prenex. \ENDDOC \DOC{SUB\_AND\_COND\_ELIM\_CONV} \TYPE {\small\verb%SUB_AND_COND_ELIM_CONV : conv%}\egroup \SYNOPSIS Eliminates natural number subtraction and conditional statements from a formula. \DESCRIBE This function eliminates natural number subtraction from a formula, but in doing so may generate conditional statements, so these are eliminated too. The conditional statements are moved up through the term and if at any point the branches of the conditional become Boolean-valued the conditional is eliminated. Subtraction operators are moved up until a relation (such as less-than) is reached. The subtraction can then be transformed into an addition. Provided the argument term is a formula, only an abstraction can prevent a conditional being moved up far enough to be eliminated. If the term is not a formula it may not be possible to eliminate the subtraction. The function is also incapable of eliminating subtractions that appear in arguments to functions other than the standard operators of arithmetic. The function is not as delicate as it could be; it tries to eliminate all conditionals in a formula when it need only eliminate those that have to be removed in order to eliminate subtraction. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #SUB_AND_COND_ELIM_CONV # "((p + 3) <= n) ==> (!m. ((m = 0) => (n - 1) | (n - 2)) > p)";; |- (p + 3) <= n ==> (!m. ((m = 0) => n - 1 | n - 2) > p) = (p + 3) <= n ==> (!m. (~(m = 0) \/ n > (1 + p)) /\ ((m = 0) \/ n > (2 + p))) #SUB_AND_COND_ELIM_CONV # "!f n. f ((SUC n = 0) => 0 | (SUC n - 1)) < (f n) + 1";; |- (!f n. (f((SUC n = 0) => 0 | (SUC n) - 1)) < ((f n) + 1)) = (!f n. (~(SUC n = 0) \/ (f 0) < ((f n) + 1)) /\ ((SUC n = 0) \/ (f((SUC n) - 1)) < ((f n) + 1))) #SUB_AND_COND_ELIM_CONV # "!f n. (\m. f ((m = 0) => 0 | (m - 1))) (SUC n) < (f n) + 1";; |- (!f n. ((\m. f((m = 0) => 0 | m - 1))(SUC n)) < ((f n) + 1)) = (!f n. ((\m. ((m = 0) => f 0 | f(m - 1)))(SUC n)) < ((f n) + 1)) \end{verbatim} } \USES Useful as a preprocessor to decision procedures which do not allow natural number subtraction in their argument formula. \SEEALSO COND_ELIM_CONV. \ENDDOC `