let ins be Instruction of SCM; :: thesis: ( InsCode ins = 0 implies ins = halt SCM )
assume A1: InsCode ins = 0 ; :: thesis: ins = halt SCM
A2: now :: thesis: not ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 }
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ; :: thesis: contradiction
then ex J being Element of Segm 9 ex a being Nat st
( ins = [J,<*a*>,{}] & J = 6 ) ;
then InsCode ins = 6 ;
hence contradiction by A1; :: thesis: verum
end;
now :: thesis: not ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} }
assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; :: thesis: contradiction
then ex I being Element of Segm 9 ex b, c being Element of Data-Locations st
( ins = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
then InsCode ins in {1,2,3,4,5} ;
hence contradiction by A1, ENUMSET1:def 3; :: thesis: verum
end;
then A3: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def 3;
now :: thesis: not ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} }
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } ; :: thesis: contradiction
then ex K being Element of Segm 9 ex a1 being Nat ex b1 being Element of Data-Locations st
( ins = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
then InsCode ins in {7,8} ;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum
end;
then ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by A3, XBOOLE_0:def 3;
then ins in {[SCM-Halt,{},{}]} by A2, XBOOLE_0:def 3;
then ins = [SCM-Halt,{},{}] by TARSKI:def 1;
hence ins = halt SCM by AMI_3:26; :: thesis: verum