( [0 ,0 ] `2 = 0 & [0 ,1] `2 = 1 & [0 ,2] `2 = 2 & [0 ,3] `2 = 3 & [0 ,4] `2 = 4 ) by MCART_1:7;
hence for b₁ being Element 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)))*> ) ) ) ; :: thesis: verum