let ins be Instruction of SCM ; ( InsCode ins = 6 implies ex loc being Element of NAT st ins = SCM-goto loc )
assume A1:
InsCode ins = 6
; ex loc being Element of NAT st ins = SCM-goto loc
now assume
ins in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} }
;
contradictionthen consider I being
Element of
Segm 9,
b,
c being
Element of
SCM-Data-Loc such that A2:
ins = [I,<*b,c*>]
and A3:
I in {1,2,3,4,5}
;
InsCode ins = I
by A2, MCART_1:7;
hence
contradiction
by A1, A3, ENUMSET1:def 3;
verum end;
then A4:
ins in ({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} }
by XBOOLE_0:def 3;
now assume
ins in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} }
;
contradictionthen consider K being
Element of
Segm 9,
a1 being
Element of
NAT ,
b1 being
Element of
SCM-Data-Loc such that A5:
ins = [K,<*a1,b1*>]
and A6:
K in {7,8}
;
InsCode ins = K
by A5, MCART_1:7;
hence
contradiction
by A1, A6, TARSKI:def 2;
verum end;
then A7:
ins in {[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 }
by A4, XBOOLE_0:def 3;
not ins in {[SCM-Halt ,{} ]}
by A1, Th37, AMI_3:71, TARSKI:def 1;
then
ins in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 }
by A7, XBOOLE_0:def 3;
then consider J being Element of Segm 9, a being Element of NAT such that
A8:
( ins = [J,<*a*>] & J = 6 )
;
reconsider loc = a as Element of NAT ;
take
loc
; ins = SCM-goto loc
thus
ins = SCM-goto loc
by A8; verum