# Metamath Proof Explorer

## Theorem algrf

Description: An algorithm is a step function F : S --> S on a state space S . An algorithm acts on an initial state A e. S by iteratively applying F to give A , ( FA ) , ( F( FA ) ) and so on. An algorithm is said to halt if a fixed point of F is reached after a finite number of iterations.

The algorithm iterator R : NN0 --> S "runs" the algorithm F so that ( Rk ) is the state after k iterations of F on the initial state A .

Domain and codomain of the algorithm iterator R . (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses algrf.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
algrf.2 ${⊢}{R}=seq{M}\left(\left({F}\circ {1}^{st}\right),\left({Z}×\left\{{A}\right\}\right)\right)$
algrf.3 ${⊢}{\phi }\to {M}\in ℤ$
algrf.4 ${⊢}{\phi }\to {A}\in {S}$
algrf.5 ${⊢}{\phi }\to {F}:{S}⟶{S}$
Assertion algrf ${⊢}{\phi }\to {R}:{Z}⟶{S}$

### Proof

Step Hyp Ref Expression
1 algrf.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 algrf.2 ${⊢}{R}=seq{M}\left(\left({F}\circ {1}^{st}\right),\left({Z}×\left\{{A}\right\}\right)\right)$
3 algrf.3 ${⊢}{\phi }\to {M}\in ℤ$
4 algrf.4 ${⊢}{\phi }\to {A}\in {S}$
5 algrf.5 ${⊢}{\phi }\to {F}:{S}⟶{S}$
6 fvconst2g ${⊢}\left({A}\in {S}\wedge {x}\in {Z}\right)\to \left({Z}×\left\{{A}\right\}\right)\left({x}\right)={A}$
7 4 6 sylan ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to \left({Z}×\left\{{A}\right\}\right)\left({x}\right)={A}$
8 4 adantr ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {A}\in {S}$
9 7 8 eqeltrd ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to \left({Z}×\left\{{A}\right\}\right)\left({x}\right)\in {S}$
10 vex ${⊢}{x}\in \mathrm{V}$
11 vex ${⊢}{y}\in \mathrm{V}$
12 10 11 algrflem ${⊢}{x}\left({F}\circ {1}^{st}\right){y}={F}\left({x}\right)$
13 simpl ${⊢}\left({x}\in {S}\wedge {y}\in {S}\right)\to {x}\in {S}$
14 ffvelrn ${⊢}\left({F}:{S}⟶{S}\wedge {x}\in {S}\right)\to {F}\left({x}\right)\in {S}$
15 5 13 14 syl2an ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {F}\left({x}\right)\in {S}$
16 12 15 eqeltrid ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}\left({F}\circ {1}^{st}\right){y}\in {S}$
17 1 3 9 16 seqf ${⊢}{\phi }\to seq{M}\left(\left({F}\circ {1}^{st}\right),\left({Z}×\left\{{A}\right\}\right)\right):{Z}⟶{S}$
18 2 feq1i ${⊢}{R}:{Z}⟶{S}↔seq{M}\left(\left({F}\circ {1}^{st}\right),\left({Z}×\left\{{A}\right\}\right)\right):{Z}⟶{S}$
19 17 18 sylibr ${⊢}{\phi }\to {R}:{Z}⟶{S}$