A1: for I being Element of F₁() st I in ElementaryInstructions F₁() holds
P₁[I] and
A2: P₁[ EmptyIns F₁()] and
A3: for I1, I2 being Element of F₁() st P₁[I1] & P₁[I2] holds
P₁[I1 \; I2] and
A4: for C, I1, I2 being Element of F₁() st P₁[C] & P₁[I1] & P₁[I2] holds
P₁[ if-then-else (C,I1,I2)] and
A5: for C, I being Element of F₁() st P₁[C] & P₁[I] holds
P₁[ while (C,I)]