A1: ( [0,2] `2 = 2 & [0,3] `2 = 3 ) by MCART_1:7;
( [0,0] `2 = 0 & [0,1] `2 = 1 ) by MCART_1:7;
hence for b₁ being XFinSequence of the Instructions 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)))%> ) ) ) by A1, MCART_1:7; :: thesis: verum