let ins be Instruction of SCM; ( InsCode ins = 7 implies ex loc being Nat ex da being Data-Location st ins = da =0_goto loc )
assume A1:
InsCode ins = 7
; ex loc being Nat ex da being Data-Location st ins = da =0_goto loc
now 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} }
;
contradictionthen consider I being
Element of
Segm 9,
b,
c being
Element of
Data-Locations such that A3:
ins = [I,{},<*b,c*>]
and A4:
I in {1,2,3,4,5}
;
InsCode ins = I
by A3;
hence
contradiction
by A1, A4, ENUMSET1:def 3;
verum end;
then A5:
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;
InsCode (halt SCM) = 0
by COMPOS_1:70;
then
not ins in {[SCM-Halt,{},{}]}
by A1, AMI_3:26, TARSKI:def 1;
then
not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 }
by A2, XBOOLE_0:def 3;
then
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} }
by A5, XBOOLE_0:def 3;
then consider K being Element of Segm 9, a1 being Nat, b1 being Element of Data-Locations such that
A6:
ins = [K,<*a1*>,<*b1*>]
and
K in {7,8}
;
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Nat ;
take
loc
; ex da being Data-Location st ins = da =0_goto loc
take
da
; ins = da =0_goto loc
thus
ins = da =0_goto loc
by A1, A6; verum