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 jIt should be clear that doing prime 1 followed by prime 2 does the overall intended function.