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