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