July 2011

A Mizar demo

PC Mizar 7.11.07_4.160.1126

In this mini-tutorial we walk over some details of developing a short proof concerning Fibonacci numbers.

The Fibonacci sequence has been previously defined in Mizar article PRE_FF as follows:

```
definition
let n be Nat;
func Fib (n) -> Element of NAT means
:: PRE_FF:def 1
ex fib being Function of NAT, [:NAT, NAT:]
st it = (fib.n)`1 & fib.0 = [0,1] &
for n being Nat holds fib.(n+1) = [(fib.n)`2, (fib.n)`1 + (fib.n)`2];
end;
```
Mizar does not permit recursive definitions of functors, therefore the above definition depends on a recursively defined set theoretic function (several schemes are available for recursive definitions of such functions). A theorem that follows, recasts the usual recursive property of the functor Fib. In the sequel, we will frequently refer to this theorem, which in other circumstances is understood as the definition of the Fibonacci sequence.
```      theorem :: PRE_FF:1
Fib(0) = 0 & Fib(1) = 1 &
for n being Nat holds Fib((n+1)+1) = Fib(n) + Fib(n+1);
```
Let us try to prove that the n-th Fibonacci number is no less than n.
```     environ  :: mt1

begin

for n being Nat holds Fib n >= n;

```
The above text is put into a .miz file and checked by the Mizar processor. Unfortunately, Mizar could not 'understand' the text in the empty environment and we got the following errors.
```     environ  :: mt1

begin

for n being Nat holds Fib n >= n;
::>                *143  *398

::> 143: No implicit qualification
::> 398: Type expected
```
The mysterious error *143 under Nat means that in this context Nat is treated as an unknown identifier. (The "No implicit qualification" comment relates to the lack of the reserve construct but we will not explain more here in order to avoid discussing constructs which we will not use.)

It is a reasonable practice for beginners to try to correct only the first parsing error, and, in general, it is advisable to deal with one error at a time.

Nat - the type of natural numbers is introduced in article NAT_1. New users find the task of searching the Mizar library for needed definitions a big challenge. A long lasting solution to the problem consists in getting familiar with the library. For the beginners, the best starting tactic is to ask someone who is more experienced. One can search the libraries using grep, but the beginners have difficulty in formulating search patterns as newcomers typically have trouble naming what they are looking for.

In order to import the needed meaning of Nat we import vocabulary NAT_1 (for the mode symbol Nat), notations from NAT_1 (for parsing formats) and constructors from NAT_1 (for semantics, i.e. internal representation of the notion). We are now left with two parsing errors.

```     environ  :: mt2
vocabularies NAT_1;
notations NAT_1;
constructors NAT_1;
begin

for n being Nat holds Fib n >= n;
::>                          *143,321

::> 143: No implicit qualification
::> 321: Predicate symbol or "is" expected
```
Mizar processes the input text and inserts error messages into the presented file in lines starting with ::>. These lines are treated as comments and are stripped off when the text is processed the next time while new error messages are usually inserted. As a result, we work with one text file which we edit and which is modified by Mizar during processing.

Error *143 indicates that Fib is treated as an identifier of a variable and in the above context such an identifier needs to have its type (qualification) announced earlier. However, our intention was that Fib denotes the functor for the Fibonacci sequence as defined in PRE_FF. That Fib is indeed a functor symbol is declared in vocabulary PRE_FF. We learned this by using the findvoc utility which we called as

```      findvoc -w Fib
```
We add vocabulary PRE_FF to the environment and obtain
```     environ  :: mt3
vocabularies NAT_1, PRE_FF;
notations NAT_1;
constructors NAT_1;
begin

for n being Nat holds Fib n >= n;
::>                          *165*203
::> 165: Unknown functor format
::> 203: Unknown token, maybe an illegal character used in an identifier
```
Fib is now known to be a functor but its parsing format and the information on how it is used to construct terms is still not in the current environment. Fib has been defined in article PRE_FF and thus we import constructors and notation from this article.
```     environ  :: mt4
vocabularies NAT_1, PRE_FF;
notations NAT_1, PRE_FF;
constructors NAT_1, PRE_FF;
begin

for n being Nat holds Fib n >= n;
::>                              *203
::> 203: Unknown token, maybe an illegal character used in an identifier
```
The term Fib n seems to be understood by Mizar but now we need to import vocabulary in which the >= is defined. The greater than or equal relation that we want to use is defined in article XXREAL_0 as a synonym for less than or equal with swapped arguments.
```definition let x,y be ext-real number;
pred x <= y means
:: XXREAL_0:def 5
... definiens omitted ...
reflexivity;
connectedness;
end;

reserve a,b,c,d for ext-real number;

notation let a,b;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;
```

We need to import notations and constructors from XXREAL_0. But this will not suffice to make the >= predicate understood. The predicate as defined in XXREAL_0 takes arguments of type ext-real number which are real numbers extended with positive and negative infinity. To use the >= predicate in our text we need to import information that the types of terms we use as arguments of >= widen to extended real numbers. This is achieved through importing registrations.

• Importing registrations from XXREAL_0 imports (among others)
```       registration
cluster natural -> ext-real number;
end;
```
which states that every natural number is also an extended real number.

• Importing registrations from ORDINAL1 imports (among others)
```       registration
cluster -> natural Element of omega;
end;
```
We need this registration because the type returned by Fib is Element of NAT. (NAT is a synonym for omega, see NUMBERS.) The above registration states that every Element of NAT has also the attribute natural. With this information, the type of Fib n widens also to an extended real due to the previous registration imported from XXREAL_0.

The last paragraph may seem mysterious but explaining more details right now would complicate the story even more.

With the newly added environment directives we arrive at the following.
```     environ  :: mt5
vocabularies XXREAL_0, NAT_1, PRE_FF;
notations NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
begin

for n being Nat holds Fib n >= n;
::>                                 *4
::> 4: This inference is not accepted
```
It seems that we have built the right conceptual environment to formulate our goal as we are left with one purely logical message. We can now focus on proving.

The proof is to be done by induction for which we employ scheme NAT_1:sch 2 (NatInd) defined in article NAT_1 as follows.

```scheme :: NAT_1:sch 2
NatInd { P[Nat] } :
for k being Nat holds P[k]
provided
P[0] and
for k be Nat st P[k] holds P[k + 1];
```
A scheme provides a pattern for obtaining theorems. From the above scheme, we get a theorem for each actual predicate used in the place of the formal predicate named P in the scheme. This formal predicate takes one natural number argument. Each application of this scheme depends on two premises corresponding to the formulas listed after provided in the scheme declaration.

In order to get access to the scheme we use the schemes directive in the environment. We also try to formulate the premises for the application of the scheme.

```     environ  :: mt6
vocabularies XXREAL_0, NAT_1, PRE_FF;
notations NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
schemes NAT_1;
begin
P1: Fib 0 >= 0;
::>          *143

P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::>                    *203

for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2);

::> 143: No implicit qualification
::> 203: Unknown token, maybe an illegal character used in an identifier
```
In the current version of Mizar, the symbol for 0 (zero) is introduced in vocabulary CARD_1 as a functor symbol. A functor using this symbol is defined as a synonym for empty set in article NUMBERS (also in CARD_1) and then redefined in NUMBERS such that 0 is typed as Element of NAT. We add vocabulary CARD_1 to the vocabularies directive and NUMBERS to notations and obtain.
```     environ  :: mt6a
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
schemes NAT_1;
begin
P1: Fib 0 >= 0;
::>               *4

P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::>                    *203

for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
::> 203: Unknown token, maybe an illegal character used in an identifier
```
Note that we did not add NUMBERS to constructors. We did not have to do this as importing constructors for NAT_1 brought the constructors from NUMBERS to our environment. However, listing NUMBERS on the constructors' list would not cause any problems.

We postpone dealing with the not accepted inference and first resolve the notational error with the symbol + for addition. First we find the vocabulary which declares + and it is ARYTM_3.

```     environ  :: mt6b
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
schemes NAT_1;
begin
P1: Fib 0 >= 0;
::>               *4

P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::>                    *103    *103

for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
::> 103: Unknown functor
```
Small constants like 1, 2 and so on up to 16 bit unsigned integers are built-in but by default are typed as set. In order to use them as natural numbers one has to use the environment directive requirements. This directive enables default processing of certain objects; we will not comment more on this feature at this point. In our case, we need requirement package named NUMERALS which provides the needed properties of small numerals. We also need requirements SUBSET on which NUMERALS depend.
The documentation of available requirement packages is very sparse; some information is contained in .abs files with the base name of the requirement package. For the list of these names see mml.txt in the doc directory of your Mizar installation.

After adding the requirements directive, we have a situation where numeral 1 is understood as a natural number and the symbol + for addition is understood as (re)defined in NAT_1. The term (n+1) is typed Element of NAT, has the attribute natural and can be used as an argument of Fib.

```     environ  :: mt7
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS;
schemes NAT_1;
begin

P1: Fib 0 >= 0;
::>               *4

P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::>                             *4

for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2);
::>                                      *23

::> 4: This inference is not accepted
::> 23: Invalid order of arguments in the instantiated predicate
```
Note how the propositions labeled P1 and P2, which form the premises of induction, are now understood but not accepted as the Mizar checker does not see why they are true without some justification.

Error *23 relates to the formal parameter of induction, the predicate P. The actual formula corresponding to this formal predicate must be explicitly stated using the defpred macro facility. We could have used a different name than P in defpred but by some coincidence we have not.

```     environ  :: mt7a
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS;
schemes NAT_1;
begin

defpred P[Nat] means Fib \$1 >= \$1;

P1: P[0];
::>         *4

P2: for n being Nat st P[n] holds P[n+1];
::>                                         *4

for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
```
This instance of defpred defines a one place predicate P such that later occurrences like P[n] are understood as Fib n >= n. In defpred, the symbol \$1 refers to the first parameter of the defined predicate; \$2 would refer to the second parameter if there was one, and so on.

We are left with logical errors only, however, we can not proceed as the inductive step is hard to prove the way it has been stated.

Fib, in its recursive properties, makes reference to two preceding values while the inductive hypothesis provides some information only about the immediate predecessor. There is a simple remedy in this case by strengthening the proposition that we prove (induction loading) and making it a conjunction of inequalities about two subsequent terms of the Fibonacci sequence. After making appropriate adjustments we are faced by the following text.

```     environ  :: mt8
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS;
schemes NAT_1;
begin

defpred P[Nat] means Fib \$1 >= \$1 & Fib (\$1+1) >= \$1+1;

P1: P[0];
::>         *4,4
P2: for n being Nat st P[n] holds P[n+1];
::>                                         *4
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
```
The first premise of the induction scheme should easily follow from the theorem PRE_FF:1 about the Fibonacci sequence. However, we get:
```     environ  :: mt9
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS;
schemes NAT_1;
begin

defpred P[Nat] means Fib \$1 >= \$1 & Fib (\$1+1) >= \$1+1;

P1: P[0] by PRE_FF:1;
::>                *144,203
P2: for n being Nat st P[n] holds P[n+1];
::>                                         *4
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
::> 144: Unknown label
::> 203: Unknown token, maybe an illegal character used in an identifier
```
Whenever we make a library reference, in this case to PRE_FF:1, the name of the article whose theorems we want to access must appear in the library directive theorems.
```     environ  :: mt10
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS;
theorems PRE_FF;
schemes NAT_1;
begin

defpred P[Nat] means Fib \$1 >= \$1 & Fib (\$1+1) >= \$1+1;

P1: P[0] by PRE_FF:1;
::>            *4
P2: for n being Nat st P[n] holds P[n+1];
::>                                         *4
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
```
The first error is due to the fact that Mizar does not see that 0+1 = 1. Mizar is able to automatically process arithmetic expressions involving equalities, but this ability becomes available when we import requirements ARITHM (which depend also on requirements BOOLE) and thus we obtain:
```     environ  :: mt10a
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS, BOOLE, ARITHM;
theorems PRE_FF;
schemes NAT_1;
begin

defpred P[Nat] means Fib \$1 >= \$1 & Fib (\$1+1) >= \$1+1;

P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1];
::>                                         *4
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
```

In order to justify the second premise of the induction scheme, we write a proof whose structure is dictated by the proposition that we are proving. The proof starts with a let since we are proving a universally quantified formula.

```     P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib n >= n & Fib (n+1) >= n+1;
thus Fib (n+1) >= n+1 by IH;
thus Fib (n+1+1) >= n+1+1;
::>                               *4
end;
```
The formula labeled IH (for Induction Hypothesis) is really P[n] expanded as defined by defpred. After making the assumption we are to prove P[n+1] which when expanded is a conjunction. We conclude each conjunct in a separate thus.

Note that in the term n+1+1 we did not insert parentheses as Mizar binary infix operators associate to the left.

In order to prove the yet unjustified conclusion, we consider two cases: either n is zero or it is bigger than zero. For this we employ the per cases construct.

```     P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib n >= n & Fib (n+1) >= n+1;
thus Fib (n+1) >= n+1 by IH;
per cases;
::>               *4
suppose S1: n = 0;
thus Fib (n+1+1) >= n+1+1;
::>                                *4
end;
suppose S1: n > 0;
thus Fib (n+1+1) >= n+1+1;
::>                                *4
end;
end;
```
The per cases construct requires justification of the disjunction of all the suppose conditions.
```          per cases by NAT_1:3;
suppose S1: n = 0;
thus Fib (n+1+1) >= n+1+1;
::>                                *4
end;
suppose S1: n > 0;
thus Fib (n+1+1) >= n+1+1;
::>                                *4
end;
```
The theorem NAT_1:3 states that for natural numbers we have:
```theorem :: NAT_1:3
0 <> i implies 0 < i;
```
We add NAT_1 to the theorems directive in order to be able to refer to this theorem.

Unfortunately, the conclusion in the first case (when n = 0) is false as Fib 2 is 1. The formula that we tried to prove was simply false and realizing this fact so late is a bit embarrassing. However, it shows that mechanical proof-checking systems may have some future ;-)

The simple remedy in our case is to upgrade the claim that we want to prove to something like: the (n+1)-th Fibonacci is not less than n. After making all the necessary changes we get.

```     environ  :: mt14
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
theorems PRE_FF, NAT_1;
schemes NAT_1;
begin

defpred P[Nat] means Fib (\$1+1) >= \$1 & Fib (\$1+1+1) >= \$1+1;

P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib (n+1) >= n & Fib (n+1+1) >= n+1;
thus Fib (n+1+1) >= n+1 by IH;
per cases by NAT_1:3;
suppose S1: n = 0;
thus Fib (n+1+1+1) >= n+1+1;
::>                                  *4
end;
suppose S1: n > 0;
thus Fib (n+1+1+1) >= n+1+1;
::>                                  *4
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
```
Please note that we added requirements REAL. In order to justify the claim labeled P1 we need the fact that 1 >= 0. This fact becomes obvious with requirements REAL. By now, we have imported all requirements available in the current version of Mizar.

The proof of the first case is immediate from PRE_FF:1 with the use of built-in calculations, and may look like:

```          suppose S1: n = 0;
Fib (0+1+1+1) = Fib (0+1) + Fib (0+1+1) by PRE_FF:1
.= 1+1 by PRE_FF:1;
hence Fib (n+1+1+1) >= n+1+1 by S1;
end;
```
In the proof of the second case we first use PRE_FF:1. Then, we add the sides of inequalities from the inductive hypothesis labeled IH. To justify this step, we refer to theorem XREAL_1:9.
```theorem :: XREAL_1:9
a <= b & c <= d implies a+c <= b+d;
```
and thus we add XREAL_1 to the theorems directive. Even with this addition we run into a new problem.
```          suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, XREAL_1:9;
::>                                                            *190
thus Fib (n+1+1+1) >= n+1+1;
::>                                  *4
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);

::> 4: This inference is not accepted
::> 190: Inaccessible theorem
```

Theorem XREAL_1:9 is about real numbers while our current environment does not import all information necessary to access the theorem. There is a utility named constr which assists us in such situations. Calling

```     constr -f text/mt15a.miz XREAL_1:9
```
informs us that we need to import constructors from XREAL_0 in order to access theorem XREAL_1:9 in our file named text/mt15a.miz. (Constructors from XREAL_0 provide internal information about attribute real.) We also import registrations from XREAL_0 which are needed to establish the relationship between real numbers and other numbers, in particular that a natural number is a real number.
Unfortunately, there is no utility, probably there can not be one, that can tell which registrations are needed in a particular context to proceed as we plan. One needs to know parts of the Mizar library.

The new environment section is now:

```     environ  :: mt16
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, XREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1, XREAL_0;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
theorems PRE_FF, NAT_1, XREAL_1;
schemes NAT_1;
begin
```

We continue proving the second case. First, we state that n is at least 1 in order to get that n+(n+1) is at least n+1+1.

```          suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, XREAL_1:9;
n >= 1 by S1, NAT_1:14; then
n+(n+1) >= n+1+1 by XREAL_1:9;
thus Fib (n+1+1+1) >= n+1+1;
::>                                  *4
end;
```
Here is the new theorem that we referred to.
```theorem :: NAT_1:14
j < 1 implies j = 0;
```
This theorem works as n >= 1 is an antonym of n < 1 and the > predicate is irreflexive (as an antonym to a reflexive predicate).

At this moment, it is enough to use transitivity of >= to complete the proof. The transitivity of less than or equal appears as a theorem in article XXREAL_0.

```theorem :: XXREAL_0:2
a <= b & b <= c implies a <= c;
```
Note that n >= 1 is a synonym for 1 <= n. The second case of our proof is completed as follows:
```          A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, XREAL_1:9;
n >= 1 by S1, NAT_1:14; then
n+(n+1) >= n+1+1 by XREAL_1:9;
hence Fib (n+1+1+1) >= n+1+1 by A, B, XXREAL_0:2;
end;
```
Here is the complete text of our development.
```     environ  :: mt18
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, XREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1, XREAL_0;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
theorems PRE_FF, NAT_1, XREAL_1, XXREAL_0;
schemes NAT_1;
begin

defpred P[Nat] means Fib (\$1+1) >= \$1 & Fib (\$1+1+1) >= \$1+1;

P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib (n+1) >= n & Fib (n+1+1) >= n+1;
thus Fib (n+1+1) >= n+1 by IH;
per cases by NAT_1:3;
suppose S1: n = 0;
Fib (0+1+1+1) = Fib (0+1) + Fib (0+1+1) by PRE_FF:1
.= 1+1 by PRE_FF:1;
hence Fib (n+1+1+1) >= n+1+1 by S1;
end;
suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, XREAL_1:9;
n >= 1 by S1, NAT_1:14; then
n+(n+1) >= n+1+1 by XREAL_1:9;
hence Fib (n+1+1+1) >= n+1+1 by A, B, XXREAL_0:2;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);
```
From the last proposition we can infer a simpler statement in which we skip the second conjunct behind P[n].
```     then for n being Nat holds Fib (n+1) >= n;
```

Look at a proof of the same theorem using complete (course of values) induction.
```     environ  :: mt_cov999
vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3;
notations NUMBERS, NAT_1, XXREAL_0, PRE_FF;
constructors  NAT_1, XXREAL_0, XREAL_0, PRE_FF;
registrations XXREAL_0, ORDINAL1, XREAL_0;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
theorems PRE_FF, NAT_1, XREAL_1, XXREAL_0;
schemes NAT_1;
begin
defpred P[Nat] means Fib (\$1+1) >= \$1;
P: for k being Nat
st for n being Nat st n < k holds P[n]
holds P[k]
proof let k be Nat; assume
IH: for n being Nat st n < k holds Fib (n+1) >= n;
per cases;
suppose k <= 1; then k = 0 or k = 0+1 by NAT_1:26;
hence Fib (k+1) >= k by PRE_FF:1;
end;
suppose 1 < k; then
1+1 <= k by NAT_1:13; then
consider m being Nat such that
A: k = 1+1+m by NAT_1:10;
thus Fib (k+1) >= k proof
per cases by NAT_1:3;
suppose S1: m = 0;
Fib (0+1+1+1) = Fib(0+1) + Fib(0+1+1) by PRE_FF:1
.= 1 + 1 by PRE_FF:1;
hence Fib (k+1) >= k by A, S1;
end;
suppose m > 0; then
m >= 1 by NAT_1:14; then
B: m+(m+1) >= m+1+1 by XREAL_1:9;
m < m+1 & m+1 < m+1+1 by XREAL_1:31; then
m < k & m+1 < k by A, XXREAL_0:2; then
C: Fib (m+1) >= m & Fib (m+1+1) >= m+1 by IH;
Fib (m+1+1+1) = Fib (m+1) + Fib (m+1+1) by PRE_FF:1; then
Fib (m+1+1+1) >= m+(m+1) by C, XREAL_1:9;
hence Fib (k+1) >= k by A, B, XXREAL_0:2;
end;
end;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 4(P);
then for n being Nat holds Fib(n+1) >= n;
```