Iterate/Loop algebra

← Back to Iterate

$c_{n}$ refers to any value independent of the current state of the block. Visit count $VC$ specifically refers to the inner body, shown with an ellipsis.

Theorem	Structure	Claim	Proof
Given	*x< ... >	$VC=x$	By definition of the loop construct.
Theorem 1	*c1< *c2< ... > >	$VC=c_{1}\cdot c_{2}$	The inner body is executed $c_{2}$ times per each outer iteration, of which there are $c_{1}$ such.
Theorem 2	*c1< ⋱ *cn< ... > ⋰ >	$VC=\prod _{i=1}^{n}{c_{i}}$	Repeated application of Theorem 1.
Theorem 3	*c< *n< ... > >	$VC=\sum _{i=1}^{c}{i}={\frac {c(c+1)}{2}}$	On the $i$-th iteration of the outer body, the inner body executes $i$ times.
Theorem 4	*c< *~n< ... > >	$VC=\sum _{i=1}^{c}{c-i}=\sum _{i=1}^{c-1}{i}={\frac {c(c-1)}{2}}$	On the $i$-th iteration of the outer body, the inner body executes $c-i$ times.
Theorem 5	*c< *~n< ... >  ! >	$VC=c-1$	By Theorem 4, the first iteration of the outer loop, VC increments by $c-1$. The break immediately halts further iterations of the outer loop.

This is still a work in progress. It may be changed in the future.