For a sequence of two primes A and B, the proof rule is:
Does doing A, followed by doing B, do the overall intended function?
Sequences are not limited to two primes. For example, the sequence A-B-C-D would use the proof rule: ``Does doing A, then B, then C, then D, do the overall I/F?''
Here's a fairly trivial example:
# [ return i + 2 ]
def addTwo ( i ):
#-- 1 --
# [ j := i + 2 ]
j = i + 2
#-- 2 --
# [ return j ]
return j
It should be clear that doing prime 1 followed by prime 2 does
the overall intended function.