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 = ( ZZ>= ` M )
	algrf.2	|- R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
	algrf.3	|- ( ph -> M e. ZZ )
	algrf.4	|- ( ph -> A e. S )
	algrf.5	|- ( ph -> F : S --> S )
Assertion	algrf	|- ( ph -> R : Z --> S )

Proof

Step	Hyp	Ref	Expression
1		algrf.1	|- Z = ( ZZ>= ` M )
2		algrf.2	|- R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
3		algrf.3	|- ( ph -> M e. ZZ )
4		algrf.4	|- ( ph -> A e. S )
5		algrf.5	|- ( ph -> F : S --> S )
6		fvconst2g	|- ( ( A e. S /\ x e. Z ) -> ( ( Z X. { A } ) ` x ) = A )
7	4 6	sylan	|- ( ( ph /\ x e. Z ) -> ( ( Z X. { A } ) ` x ) = A )
8	4	adantr	|- ( ( ph /\ x e. Z ) -> A e. S )
9	7 8	eqeltrd	|- ( ( ph /\ x e. Z ) -> ( ( Z X. { A } ) ` x ) e. S )
10		vex	|- x e. _V
11		vex	|- y e. _V
12	10 11	opco1i	|- ( x ( F o. 1st ) y ) = ( F ` x )
13		simpl	|- ( ( x e. S /\ y e. S ) -> x e. S )
14		ffvelrn	|- ( ( F : S --> S /\ x e. S ) -> ( F ` x ) e. S )
15	5 13 14	syl2an	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( F ` x ) e. S )
16	12 15	eqeltrid	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x ( F o. 1st ) y ) e. S )
17	1 3 9 16	seqf	|- ( ph -> seq M ( ( F o. 1st ) , ( Z X. { A } ) ) : Z --> S )
18	2	feq1i	|- ( R : Z --> S <-> seq M ( ( F o. 1st ) , ( Z X. { A } ) ) : Z --> S )
19	17 18	sylibr	|- ( ph -> R : Z --> S )