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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	algrf.2	⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
	algrf.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	algrf.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	algrf.5	⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ 𝑆 )
Assertion	algrf	⊢ ( 𝜑 → 𝑅 : 𝑍 ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		algrf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		algrf.2	⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
3		algrf.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		algrf.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5		algrf.5	⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ 𝑆 )
6		fvconst2g	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
7	4 6	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ 𝑆 )
9	7 8	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑥 ) ∈ 𝑆 )
10		vex	⊢ 𝑥 ∈ V
11		vex	⊢ 𝑦 ∈ V
12	10 11	opco1i	⊢ ( 𝑥 ( 𝐹 ∘ 1st ) 𝑦 ) = ( 𝐹 ‘ 𝑥 )
13		simpl	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
14		ffvelcdm	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑆 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
15	5 13 14	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
16	12 15	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( 𝐹 ∘ 1st ) 𝑦 ) ∈ 𝑆 )
17	1 3 9 16	seqf	⊢ ( 𝜑 → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) : 𝑍 ⟶ 𝑆 )
18	2	feq1i	⊢ ( 𝑅 : 𝑍 ⟶ 𝑆 ↔ seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) : 𝑍 ⟶ 𝑆 )
19	17 18	sylibr	⊢ ( 𝜑 → 𝑅 : 𝑍 ⟶ 𝑆 )