-- ITER1ITER2


Derivation of

iter1(F,N) ~ iter2(F,N)

Applying the theorem

s = map(loop(f)(0))(s)

at position [1] of the preceding tree leads to the formula

Any f0:
(iter1(F,N) ~ map(loop(f0)(0))(iter2(F,N)))

Applying the theorem

map(loop(f)(n))(iter2(f,x)) = iter1(f,loop(f)(n)(x))

at position [0,1] of the preceding tree leads to the formula

Any f0:
(  iter1(f0,N) ~ iter1(f0,loop(f0)(0)(N))
 & F = f0)

Simplifying (2 steps) the preceding tree leads to the formula

iter1(F,N) ~ iter1(F,loop(F)(0)(N))

Applying the axiom

loop(f)(0)(x) = x

at position [1,1] of the preceding tree leads to the formula

iter1(F,N) ~ iter1(F,N)

Simplifying the entire formula leads to True.