( [0,0] `2 = 0 & [0,1] `2 = 1 & [0,2] `2 = 2 & [0,3] `2 = 3 & [0,4] `2 = 4 )
;
hence
for b1 being XFinSequence of the InstructionsF of SCM holds
( ( nt = [0,0] & nt = [0,1] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,2] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,3] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,4] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,1] & nt = [0,2] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,3] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,4] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,2] & nt = [0,3] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,2] & nt = [0,4] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,3] & nt = [0,4] implies ( b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) )
; verum