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={\mathbb{Z}}_{\ge M}$$
	algrf.2	$$⊢R=seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)$$
	algrf.3	$$⊢\phi \to M\in \mathbb{Z}$$
	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={\mathbb{Z}}_{\ge M}$$
2		algrf.2	$$⊢R=seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)$$
3		algrf.3	$$⊢\phi \to M\in \mathbb{Z}$$
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\times \left\{A\right\}\right)\left(x\right)=A$$
7	4 6	sylan	$$⊢\left(\phi \wedge x\in Z\right)\to \left(Z\times \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\times \left\{A\right\}\right)\left(x\right)\in S$$
10		vex	$$⊢x\in \mathrm{V}$$
11		vex	$$⊢y\in \mathrm{V}$$
12	10 11	opco1i	$$⊢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		ffvelcdm	$$⊢\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 seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right):Z⟶S$$
18	2	feq1i	$$⊢R:Z⟶S\leftrightarrow seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right):Z⟶S$$
19	17 18	sylibr	$$⊢\phi \to R:Z⟶S$$