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